Documentation

MathlibNt.AnalyticNumberTheory.Vaughan.VaughanAllCharacterAnalyticLedger

All-character nonprincipal Vaughan ledger and Type-II scale audit #

This module only assembles proved producers. It keeps the principal character out, keeps the full prefix maximum on the all-character side, and records that the currently proved tensor Type-II estimate is only an endpoint estimate. Consequently no Standard Bombieri--Vinogradov theorem is claimed.

source
def AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff :
ℤ → ℂ

The coefficient 1, used to specialize Vaughan's identity to Λ.

Equations
Instances For
    source
    noncomputable def AnalyticNumberTheory.LargeSieve.vaughanConductorPrefixLane (a : ℤ → ℂ) (N Q : ℕ) :
    ℝ

    One conductor-weighted primitive prefix-maximal lane.

    Equations
    Instances For
      source
      noncomputable def AnalyticNumberTheory.LargeSieve.vaughanLambdaConductorCorrectionScale (N Q : ℕ) :
      ℝ

      The closed Λ-specific conductor correction, with every N,Q,log factor kept literal.

      Equations
      Instances For
        source
        theorem AnalyticNumberTheory.LargeSieve.vaughanLambdaCoeff_unit_eq (n : ℤ) :
        vaughanLambdaCoeff vaughanUnitIntegerCoeff n = vonMangoldtIntegerCoeff n
        source
        theorem AnalyticNumberTheory.LargeSieve.weighted_allCharacter_nonprincipal_vaughan_analytic_ledger (N Q u v : ℕ) :
        ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, characterPrefixMaxSquare χ vonMangoldtIntegerCoeff 0 N ≤ 6 * (vaughanConductorPrefixLane (vaughanTypeICoeff vaughanUnitIntegerCoeff u v) N Q + vaughanConductorPrefixLane (vaughanTypeIICoeff vaughanUnitIntegerCoeff u v) N Q + vaughanConductorPrefixLane (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N Q) + vaughanLambdaConductorCorrectionScale N Q

        The real all-character, nonprincipal Vaughan ledger. This theorem combines (1) exact conductor grouping, (2) the full prefix-maximal three-piece Vaughan identity, and (3) the proved Λ-specific Q² polylog change-level correction. The principal character is absent from the left side and is not estimated here.

        source
        noncomputable def AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale (N Q C k B : ℕ) :
        ℝ

        The exact endpoint-only Type-II scale delivered by the current producers on one conductor window C ≤ conductor ≤ 2C and one Vaughan outer shell 2^k. It includes, in order: linear imprimitive transport, outer Möbius Cauchy, the primitive large-sieve charge, and the unconditional constant-27 tensor moment.

        Equations
        Instances For
          source
          theorem AnalyticNumberTheory.LargeSieve.weighted_imprimitive_vaughanTypeII_endpoint_window_unconditional (N Q C u v k l B : ℕ) (hC : 0 < C) (hB : ∀ n ≤ N, ‖vaughanUnitIntegerCoeff ↑n‖ ≤ ↑B) :
          ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, ‖vaughanTypeIICanonicalBilinearBlock (fun (x : ℕ) => 1) N N u v k l d ψ‖ ^ 2 ≤ existingTypeIIEndpointWindowScale N Q C k B

          Actual assembly of the current Type-II producers. This is deliberately an endpoint square at y=N, not a maximum over all prefixes.

          source
          theorem AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale_split (N Q C k B : ℕ) :
          existingTypeIIEndpointWindowScale N Q C k B = 27 * ↑B ^ 2 * ↑(Q / C) * conductorHarmonicFactor (Q / C) * ↑(2 ^ k) * Real.log ↑(N + 1) ^ 5 * (↑N ^ 2 + ↑N * ((2 * ↑⌈Real.log (↑(2 * C) ^ 2) / Real.log 2⌉₊ + 12) * ↑(2 * C) ^ 2))

          Algebraic payment audit: the length term of the primitive large sieve pays N a second time after the tensor moment has already paid its physical row mass N; the outer-shell Cauchy separately pays 2^k.

          source
          theorem AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale_not_BV_saving (N Q C k B A : ℕ) (hN : 0 < N) (hBC : C ≤ Q) (hC : 0 < C) (hB : 0 < B) (hlog : 1 < Real.log ↑(N + 1) ^ A) :
          ¬existingTypeIIEndpointWindowScale N Q C k B ≤ ↑B ^ 2 * ↑N ^ 2 / Real.log ↑(N + 1) ^ A

          Formal scale obstruction. Once every non-log factor is at least one, the current endpoint Type-II route is at least 27 B² N² log(N+1)^5; hence it cannot supply an inverse-log saving over the square-mean BV benchmark B²N²/log^A. This is a statement about this produced majorant, not a lower bound on the true character sum.

          source
          def AnalyticNumberTheory.LargeSieve.VaughanTypeIIPrefixTensorRepair (N Q u v A : ℕ) (K : ℝ) :
          Prop

          Minimal missing Type-II interface. Unlike the proved endpoint theorem, this contract retains the maximum over every prefix before summing over characters and conductors, and it asks for the inverse-log square-mean scale with no repeated outer-shell/row-length payment. It is intentionally a named Prop, not asserted as a theorem.

          Equations
          Instances For