Standard BV through a low/high primitive-conductor split

This module keeps three logically different inputs separate.

• PrimitivePrefixSiegelWalfiszSource is the minimal low-conductor source: a pointwise bound for a primitive twisted Λ prefix. It is not a BV statement.
• Above R = floor(log(N)^C) all direct means remain literal finite sums.
• The Standard-BV endpoint is obtained only after the principal, prime-power, and partial-summation physical terms have all been paid.

The weighted-Cauchy lemma below records the only automatic effect of deleting conductors ≤ R: the outer factor is the harmonic tail sum_{R<d≤Q} 1/d. There is no factor R⁻¹. Consequently the needed inverse-log saving is located explicitly in VaughanHighConductorHybridSaving, not attributed to Cauchy or to the choice of the modulus exponent B.

noncomputable def AnalyticNumberTheory.LargeSieve.logConductorThreshold (N C : ℕ) : ℕ

The literal low/high separator R = floor(log(N)^C).

Equations

• AnalyticNumberTheory.LargeSieve.logConductorThreshold N C = ⌊Real.log ↑N ^ C⌋₊

noncomputable def AnalyticNumberTheory.LargeSieve.lowConductorSet (N Q C : ℕ) : Finset ℕ

Primitive conductors from two through the logarithmic separator.

Equations

• AnalyticNumberTheory.LargeSieve.lowConductorSet N Q C = {d ∈ Finset.Icc 2 Q | d ≤ AnalyticNumberTheory.LargeSieve.logConductorThreshold N C}

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorSet (N Q C : ℕ) : Finset ℕ

Primitive conductors strictly above the logarithmic separator.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorSet N Q C = {d ∈ Finset.Icc 2 Q | AnalyticNumberTheory.LargeSieve.logConductorThreshold N C < d}

theorem AnalyticNumberTheory.LargeSieve.lowConductorSet_disjoint_highConductorSet (N Q C : ℕ) : Disjoint (lowConductorSet N Q C) (highConductorSet N Q C)

theorem AnalyticNumberTheory.LargeSieve.lowConductorSet_union_highConductorSet (N Q C : ℕ) : lowConductorSet N Q C ∪ highConductorSet N Q C = Finset.Icc 2 Q

noncomputable def AnalyticNumberTheory.LargeSieve.directConductorMeanOn (a : ℤ → ℂ) (N Q : ℕ) (S : Finset ℕ) : ℝ

Direct conductor sum on an arbitrary conductor set.

Equations

• AnalyticNumberTheory.LargeSieve.directConductorMeanOn a N Q S = ∑ d ∈ S, AnalyticNumberTheory.LargeSieve.directConductorWeight Q d * ∑ ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude a N d ψ

noncomputable def AnalyticNumberTheory.LargeSieve.lowConductorPhysical (N Q C : ℕ) : ℝ

Low-conductor physical term after exact all-character regrouping.

Equations

• AnalyticNumberTheory.LargeSieve.lowConductorPhysical N Q C = AnalyticNumberTheory.LargeSieve.directConductorMeanOn AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff N Q (AnalyticNumberTheory.LargeSieve.lowConductorSet N Q C)

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorPhysical (N Q C : ℕ) : ℝ

High-conductor physical term. No estimate is built into this definition.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorPhysical N Q C = AnalyticNumberTheory.LargeSieve.directConductorMeanOn AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff N Q (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)

theorem AnalyticNumberTheory.LargeSieve.directConductorMean_low_high (a : ℤ → ℂ) (N Q C : ℕ) : ∑ d ∈ Finset.Icc 2 Q, directConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitivePrefixAmplitude a N d ψ = directConductorMeanOn a N Q (lowConductorSet N Q C) + directConductorMeanOn a N Q (highConductorSet N Q C)

Exact low/high partition of the conductor-regrouped direct mean.

def AnalyticNumberTheory.LargeSieve.PrimitivePrefixSiegelWalfiszSource : Prop

Minimal Siegel--Walfisz primitive-prefix source. It controls each primitive Λ twist at conductor d ≤ log(N)^C; no modulus average and no BV conclusion occurs in its type. The decay exponent D is chosen after C.

Equations

• AnalyticNumberTheory.LargeSieve.PrimitivePrefixSiegelWalfiszSource = ∀ (C D : ℕ), ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∀ d ∈ Finset.Icc 2 (AnalyticNumberTheory.LargeSieve.logConductorThreshold N C), ∀ (ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d), AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff N d ψ ≤ K * ↑N / Real.log ↑N ^ D

noncomputable def AnalyticNumberTheory.LargeSieve.lowConductorArithmeticMass (N Q C : ℕ) : ℝ

The exact finite arithmetic mass multiplying a pointwise SW estimate.

Equations

• AnalyticNumberTheory.LargeSieve.lowConductorArithmeticMass N Q C = ∑ d ∈ AnalyticNumberTheory.LargeSieve.lowConductorSet N Q C, AnalyticNumberTheory.LargeSieve.directConductorWeight Q d * ↑(Fintype.card (AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d))

theorem AnalyticNumberTheory.LargeSieve.lowConductorPhysical_le_of_primitivePrefix (N Q C : ℕ) (X : ℝ) (_hX : 0 ≤ X) (hSW : ∀ d ∈ lowConductorSet N Q C, ∀ (ψ : PrimitiveCharacter d), primitivePrefixAmplitude vonMangoldtIntegerCoeff N d ψ ≤ X) : lowConductorPhysical N Q C ≤ lowConductorArithmeticMass N Q C * X

A primitive-prefix SW bound pays the low-conductor physical term with its literal conductor multiplicity and character count.

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn (a : ℤ → ℂ) (N : ℕ) (S : Finset ℕ) : ℝ

AP-normalized primitive direct mean restricted to a conductor set.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn a N S = ∑ d ∈ S, (↑d.totient)⁻¹ * ∑ ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude a N d ψ

noncomputable def AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn (a : ℤ → ℂ) (N : ℕ) (S : Finset ℕ) : ℝ

Square-large-sieve ledger on exactly the same conductor set.

Equations

• AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn a N S = ∑ d ∈ S, ↑d / ↑d.totient * ∑ ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare a 0 N d ψ

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor (Q R : ℕ) : ℝ

The genuine weighted-Cauchy outer payment after deleting conductors ≤ R.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor Q R = ∑ d ∈ Finset.Icc (R + 1) Q, (↑d)⁻¹

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_high_sq_le (a : ℤ → ℂ) (N Q R : ℕ) (hcard : ∀ d ∈ Finset.Icc (R + 1) Q, Fintype.card (PrimitiveCharacter d) ≤ d.totient) : apNormalizedPrimitiveMeanOn a N (Finset.Icc (R + 1) Q) ^ 2 ≤ highConductorHarmonicFactor Q R * primitivePrefixSquareLedgerOn a N (Finset.Icc (R + 1) Q)

Weighted Cauchy on the high-conductor interval. The lower cutoff produces exactly the harmonic tail, while d/φ(d) occurs only in the square ledger.

theorem AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor_le (Q R : ℕ) : highConductorHarmonicFactor Q R ≤ conductorHarmonicFactor Q

Removing low conductors only deletes positive harmonic summands.

theorem AnalyticNumberTheory.LargeSieve.inv_Q_le_highConductorHarmonicFactor {Q R : ℕ} (hRQ : R < Q) : (↑Q)⁻¹ ≤ highConductorHarmonicFactor Q R

If the high range is nonempty, its Cauchy factor still contains the final summand 1/Q. Thus Cauchy supplies no automatic power of R; any useful inverse-log gain must enter the high-conductor analytic estimate itself.

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIMean (N Q C u v : ℕ) : ℝ

Exact high-conductor Type-I direct mean.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIMean N Q C u v = AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean (N Q C u v : ℕ) : ℝ

Exact high-conductor Type-II direct mean.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean N Q C u v = AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean (N Q C v : ℕ) : ℝ

Exact high-conductor small Vaughan mean.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean N Q C v = AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn (AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff v) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)

def AnalyticNumberTheory.LargeSieve.VaughanHighConductorHybridSaving (N Q C u v : ℕ) (X : ℝ) : Prop

The missing analytic saving is frozen at its real location: the sum of the three exact high-conductor Vaughan means. This is not a BV conclusion.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanHighConductorHybridSaving N Q C u v X = (AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIMean N Q C u v + AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean N Q C u v + AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean N Q C v ≤ X)

structure AnalyticNumberTheory.LargeSieve.StandardBVPhysicalTerms : Type

Exact physical terms appearing after principal reduction and discrete partial summation. nonprincipal is where the low/high conductor route feeds in; all other lanes are already concrete.

• nonprincipal : ℝ
• principal : ℝ
• principalBad : ℝ
• primePower : ℝ
• chebyshevToLi : ℝ

def AnalyticNumberTheory.LargeSieve.StandardBVPhysicalTerms.total (P : StandardBVPhysicalTerms) (abel : ℝ) : ℝ

Literal total physical payment after the Abel amplifier.

Equations

• P.total abel = abel * (P.nonprincipal + P.principal + P.principalBad + P.primePower) + P.chebyshevToLi

noncomputable def AnalyticNumberTheory.LargeSieve.nonprincipalLambdaPhysical (N Q : ℕ) : ℝ

Exact nonprincipal character term produced by the finite AP orthogonality theorem.

Equations

• AnalyticNumberTheory.LargeSieve.nonprincipalLambdaPhysical N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q, AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefixMaxAmplitude N q χ

noncomputable def AnalyticNumberTheory.LargeSieve.principalGlobalPhysical (N Q : ℕ) : ℝ

Exact principal modulus-one term, with its 1/φ(q) transport retained.

Equations

• AnalyticNumberTheory.LargeSieve.principalGlobalPhysical N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError N 1

noncomputable def AnalyticNumberTheory.LargeSieve.principalBadPhysical (N Q : ℕ) : ℝ

Exact bad-prime-power deletion from the principal characters.

Equations

• AnalyticNumberTheory.LargeSieve.principalBadPhysical N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * (↑q.log2 * (↑N.log2 + 1) * Real.log ↑N)

noncomputable def AnalyticNumberTheory.LargeSieve.primePowerPhysical (N Q : ℕ) : ℝ

Exact higher-prime-power correction in the ψ-to-prime passage.

Equations

• AnalyticNumberTheory.LargeSieve.primePowerPhysical N Q = ∑ q ∈ Finset.Icc 1 Q, AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrectionPrefixMaxError N q

noncomputable def AnalyticNumberTheory.LargeSieve.chebyshevToLiPhysical (N Q : ℕ) : ℝ

Exact scalar discrete-main-to-li source after summing 1/φ(q).

Equations

• AnalyticNumberTheory.LargeSieve.chebyshevToLiPhysical N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourcePrefixMaxError N

noncomputable def AnalyticNumberTheory.LargeSieve.concreteStandardBVPhysicalTerms (N Q : ℕ) : StandardBVPhysicalTerms

The literal five-lane packet supplied by character orthogonality, principal reduction, prime-power removal, and partial summation.

Equations

• AnalyticNumberTheory.LargeSieve.concreteStandardBVPhysicalTerms N Q = { nonprincipal := AnalyticNumberTheory.LargeSieve.nonprincipalLambdaPhysical N Q, principal := AnalyticNumberTheory.LargeSieve.principalGlobalPhysical N Q, principalBad := AnalyticNumberTheory.LargeSieve.principalBadPhysical N Q, primePower := AnalyticNumberTheory.LargeSieve.primePowerPhysical N Q, chebyshevToLi := AnalyticNumberTheory.LargeSieve.chebyshevToLiPhysical N Q }

theorem AnalyticNumberTheory.LargeSieve.sum_standardPrimeAPPrefixMaxError_le_concretePhysical (N Q : ℕ) (hN : 2 ≤ N) : ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ (concreteStandardBVPhysicalTerms N Q).total (discreteAbelAmplifierPrefixMax N)

The proven finite principal/prime-power/partial-summation connector. No analytic estimate is used here.

def AnalyticNumberTheory.LargeSieve.LambdaToLowHighConductorConnector (N Q C : ℕ) : Prop

The remaining finite normalization connector needed to feed the conductor split into the preceding concrete packet. Its statement is an inequality between literal finite means, not an analytic or BV hypothesis.

Equations

• AnalyticNumberTheory.LargeSieve.LambdaToLowHighConductorConnector N Q C = (AnalyticNumberTheory.LargeSieve.nonprincipalLambdaPhysical N Q ≤ 2 * (AnalyticNumberTheory.LargeSieve.lowConductorPhysical N Q C + AnalyticNumberTheory.LargeSieve.highConductorPhysical N Q C) + 2 * AnalyticNumberTheory.LargeSieve.directConductorCorrectionMean AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff N Q)

theorem AnalyticNumberTheory.LargeSieve.standardBV_sufficient_at (A : ℝ) (B C N Q : ℕ) (K : ℝ) (P : StandardBVPhysicalTerms) (hQ : Q = MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B) (_hconnector : LambdaToLowHighConductorConnector N Q C) (hcomponents : ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ P.total (discreteAbelAmplifierPrefixMax N)) (hpay : P.total (discreteAbelAmplifierPrefixMax N) ≤ K * ↑N / Real.log ↑N ^ A) : ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B), MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ K * ↑N / Real.log ↑N ^ A

At a fixed N,Q, a Standard-BV estimate follows once every named physical lane is dominated and their literal total fits the target. The theorem does not allow the modulus exponent B to pay a Q-independent N term: such a term remains in P.nonprincipal until the Vaughan hybrid hypothesis saves it.

def AnalyticNumberTheory.LargeSieve.StandardBVSufficient : Prop

Quantifier-faithful sufficient interface for Standard BV. For each target A, choose the conductor exponent C; then choose the modulus exponent B. The producer must pay all five physical lanes uniformly for large N. This ordering makes explicit that increasing B cannot repair a missing Q-independent high-conductor N saving.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVSufficient = ∀ (A : ℝ), 0 < A → ∃ (C : ℕ) (B : ℕ) (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∃ (P : AnalyticNumberTheory.LargeSieve.StandardBVPhysicalTerms), AnalyticNumberTheory.LargeSieve.LambdaToLowHighConductorConnector N (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B) C ∧ ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B), MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ P.total (AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N) ∧ P.total (AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N) ≤ K * ↑N / Real.log ↑N ^ A

theorem AnalyticNumberTheory.LargeSieve.standardBV_of_sufficient (h : StandardBVSufficient) (A : ℝ) : 0 < A → ∃ (_C : ℕ) (B : ℕ) (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B), MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ K * ↑N / Real.log ↑N ^ A

The sufficient interface has exactly the usual Standard-BV conclusion.