Discrete partial summation from Chebyshev AP errors to prime AP errors

This module is deliberately downstream of the proved finite character orthogonality module. It does not assume a Bombieri--Vinogradov conclusion. The only separately packaged source term is the scalar comparison between the discrete Abel main term and the genuine logarithmic integral.

def AnalyticNumberTheory.LargeSieve.realPrefix (c : ℕ → ℝ) (y : ℕ) : ℝ

Inclusive partial sum through y.

Equations

• AnalyticNumberTheory.LargeSieve.realPrefix c y = ∑ n ∈ Finset.range (y + 1), c n

theorem AnalyticNumberTheory.LargeSieve.sum_range_mul_eq_discreteAbel (c w : ℕ → ℝ) (y : ℕ) : ∑ n ∈ Finset.range (y + 1), w n * c n = w y * realPrefix c y + ∑ n ∈ Finset.range y, (w n - w (n + 1)) * realPrefix c n

Finite discrete Abel summation, including both endpoints.

noncomputable def AnalyticNumberTheory.LargeSieve.reciprocalLogWeight (n : ℕ) : ℝ

Reciprocal-log weight with the low endpoint made total.

Equations

• AnalyticNumberTheory.LargeSieve.reciprocalLogWeight n = if 2 ≤ n then (Real.log ↑n)⁻¹ else 0

noncomputable def AnalyticNumberTheory.LargeSieve.primeThetaAPIncrement (q a n : ℕ) : ℝ

The logarithmically weighted prime increment in one residue class.

Equations

• AnalyticNumberTheory.LargeSieve.primeThetaAPIncrement q a n = if Nat.Prime n ∧ n ≡ a [MOD q] then Real.log ↑n else 0

def AnalyticNumberTheory.LargeSieve.primeAPIncrement (q a n : ℕ) : ℝ

The ordinary prime indicator in one residue class.

Equations

• AnalyticNumberTheory.LargeSieve.primeAPIncrement q a n = if Nat.Prime n ∧ n ≡ a [MOD q] then 1 else 0

noncomputable def AnalyticNumberTheory.LargeSieve.primeThetaAPPrefix (y q a : ℕ) : ℝ

The Chebyshev theta-prefix (primes only, weighted by log p).

Equations

• AnalyticNumberTheory.LargeSieve.primeThetaAPPrefix y q a = AnalyticNumberTheory.LargeSieve.realPrefix (AnalyticNumberTheory.LargeSieve.primeThetaAPIncrement q a) y

theorem AnalyticNumberTheory.LargeSieve.reciprocalLogWeight_mul_primeThetaAPIncrement (q a n : ℕ) : reciprocalLogWeight n * primeThetaAPIncrement q a n = primeAPIncrement q a n

Multiplication by 1 / log p removes the prime logarithmic weight.

theorem AnalyticNumberTheory.LargeSieve.cast_primesInAP_eq_sum_primeAPIncrement (y q a : ℕ) : ↑(MathlibNt.SieveTheory.BombieriVinogradov.primesInAP y q a) = ∑ n ∈ Finset.range (y + 1), primeAPIncrement q a n

Prime counting is the finite sum of the ordinary AP indicators.

theorem AnalyticNumberTheory.LargeSieve.primesInAP_eq_discreteAbel (y q a : ℕ) : ↑(MathlibNt.SieveTheory.BombieriVinogradov.primesInAP y q a) = reciprocalLogWeight y * primeThetaAPPrefix y q a + ∑ n ∈ Finset.range y, (reciprocalLogWeight n - reciprocalLogWeight (n + 1)) * primeThetaAPPrefix n q a

Exact discrete Abel formula for prime counting. The terms at 0 and 1 vanish because there are no primes there; no singular logarithm is evaluated.

noncomputable def AnalyticNumberTheory.LargeSieve.discreteAbelLiMain (y : ℕ) : ℝ

The deterministic main term obtained by applying the same finite Abel operator to the Chebyshev main prefix y.

Equations

• AnalyticNumberTheory.LargeSieve.discreteAbelLiMain y = AnalyticNumberTheory.LargeSieve.reciprocalLogWeight y * ↑y + ∑ n ∈ Finset.range y, (AnalyticNumberTheory.LargeSieve.reciprocalLogWeight n - AnalyticNumberTheory.LargeSieve.reciprocalLogWeight (n + 1)) * ↑n

noncomputable def AnalyticNumberTheory.LargeSieve.discreteAbelAmplifier (y : ℕ) : ℝ

The total variation of the finite Abel operator. Keeping this exact finite quantity makes the estimates valid also at y = 0,1,2.

Equations

• AnalyticNumberTheory.LargeSieve.discreteAbelAmplifier y = |AnalyticNumberTheory.LargeSieve.reciprocalLogWeight y| + ∑ n ∈ Finset.range y, |AnalyticNumberTheory.LargeSieve.reciprocalLogWeight n - AnalyticNumberTheory.LargeSieve.reciprocalLogWeight (n + 1)|

noncomputable def AnalyticNumberTheory.LargeSieve.thetaAPMainError (y q a : ℕ) : ℝ

Theta error in one reduced residue class.

Equations

• AnalyticNumberTheory.LargeSieve.thetaAPMainError y q a = AnalyticNumberTheory.LargeSieve.primeThetaAPPrefix y q a - (↑q.totient)⁻¹ * ↑y

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrection (y q a : ℕ) : ℂ

Exact higher-prime-power correction between ψ (the von Mangoldt prefix) and θ (the sum of log p over primes).

Equations

• AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrection y q a = AnalyticNumberTheory.LargeSieve.lambdaAPPrefix y q a - ↑(AnalyticNumberTheory.LargeSieve.primeThetaAPPrefix y q a)

theorem AnalyticNumberTheory.LargeSieve.lambdaAPPrefix_sub_primePowerCorrection (y q a : ℕ) : lambdaAPPrefix y q a - lambdaPrimePowerCorrection y q a = ↑(primeThetaAPPrefix y q a)

The correction is exactly what must be removed from the von Mangoldt prefix to leave the prime-only logarithmic weight.

theorem AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrection_eq_nonprime_sum (y q a : ℕ) : lambdaPrimePowerCorrection y q a = ∑ n ∈ Finset.range (y + 1), if ↑n = ↑a ∧ ¬Nat.Prime n then lambdaNatCoeff n else 0

The correction has the promised arithmetic content: it is precisely the von Mangoldt mass on non-primes in the residue class (hence, by the support of Λ, on higher prime powers).

theorem AnalyticNumberTheory.LargeSieve.abs_thetaAPMainError_le_lambda_add_primePower (y q a : ℕ) : |thetaAPMainError y q a| ≤ ‖lambdaAPMainError y q a‖ + ‖lambdaPrimePowerCorrection y q a‖

Pointwise conversion of a ψ AP error into a θ AP error, paying the higher-prime-power correction explicitly.

noncomputable def AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError (y : ℕ) : ℝ

The genuine-li source discrepancy. This is a one-dimensional global source term, independent of the modulus and residue; no AP conclusion is hidden in it.

Equations

• AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError y = |AnalyticNumberTheory.LargeSieve.discreteAbelLiMain y - MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral ↑y|

theorem AnalyticNumberTheory.LargeSieve.abs_discreteAbel_le (E : ℕ → ℝ) (M : ℝ) (y : ℕ) (hE : ∀ n ≤ y, |E n| ≤ M) : |reciprocalLogWeight y * E y + ∑ n ∈ Finset.range y, (reciprocalLogWeight n - reciprocalLogWeight (n + 1)) * E n| ≤ discreteAbelAmplifier y * M

Absolute-value estimate for the finite Abel operator under a uniform prefix bound. This is the discrete partial-summation inequality used below.

noncomputable def AnalyticNumberTheory.LargeSieve.thetaAPResiduePrefixMaxError (N q a : ℕ) : ℝ

The largest theta-prefix error for one residue through N.

Equations

• AnalyticNumberTheory.LargeSieve.thetaAPResiduePrefixMaxError N q a = (Finset.image (fun (y : ℕ) => |AnalyticNumberTheory.LargeSieve.thetaAPMainError y q a|) (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.abs_thetaAPMainError_le_residuePrefixMax {y N q a : ℕ} (hy : y ≤ N) : |thetaAPMainError y q a| ≤ thetaAPResiduePrefixMaxError N q a

theorem AnalyticNumberTheory.LargeSieve.abs_standardPrimeAPError_le_abel {y q a : ℕ} (hq : 0 < q) : |MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError y q a| ≤ discreteAbelAmplifier y * thetaAPResiduePrefixMaxError y q a + (↑q.totient)⁻¹ * globalChebyshevToLiSourceError y

Exact pointwise discrete partial-summation bound before taking maxima.

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrectionPrefixMaxError (N q : ℕ) : ℝ

Prefix maximum of the explicit higher-prime-power correction.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrectionPrefixMaxError N q = (insert 0 (Finset.image (fun (p : ℕ × ℕ) => ‖AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrection p.1 q p.2‖) ((Finset.range (N + 1)).product (AnalyticNumberTheory.Sieve.unitResidues q)))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax (N : ℕ) : ℝ

Prefix maximum of the total variation of the Abel kernel.

Equations

• AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N = (Finset.image AnalyticNumberTheory.LargeSieve.discreteAbelAmplifier (Finset.range (N + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourcePrefixMaxError (N : ℕ) : ℝ

Prefix maximum of the one-dimensional genuine-li source discrepancy.

Equations

• AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourcePrefixMaxError N = (Finset.image AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax_nonneg (N : ℕ) : 0 ≤ discreteAbelAmplifierPrefixMax N

theorem AnalyticNumberTheory.LargeSieve.thetaAPResiduePrefixMaxError_le_lambda_add_primePower {N q a : ℕ} (ha : a ∈ Sieve.unitResidues q) : thetaAPResiduePrefixMaxError N q a ≤ lambdaAPPrefixMaxError N q + lambdaPrimePowerCorrectionPrefixMaxError N q

Uniform theta-prefix control obtained from all von Mangoldt AP prefixes and the explicit higher-prime-power correction.

theorem AnalyticNumberTheory.LargeSieve.abs_standardPrimeAPError_le_prefix_bridge {y N q a : ℕ} (hq : 0 < q) (hy : y ≤ N) (ha : a ∈ Sieve.unitResidues q) : |MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError y q a| ≤ discreteAbelAmplifierPrefixMax N * (lambdaAPPrefixMaxError N q + lambdaPrimePowerCorrectionPrefixMaxError N q) + (↑q.totient)⁻¹ * globalChebyshevToLiSourcePrefixMaxError N

Pointwise prime-AP error controlled uniformly by the lambda AP prefix maximum, prime powers, and the scalar genuine-li source term.

theorem AnalyticNumberTheory.LargeSieve.standardPrimeAPPrefixMaxError_le_lambda_bridge {N q : ℕ} (hq : 0 < q) : MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ discreteAbelAmplifierPrefixMax N * (lambdaAPPrefixMaxError N q + lambdaPrimePowerCorrectionPrefixMaxError N q) + (↑q.totient)⁻¹ * globalChebyshevToLiSourcePrefixMaxError N

Lambda-to-prime AP prefix-max bridge. This is the requested finite partial-summation conclusion, connected literally to standardPrimeAPPrefixMaxError. It assumes no BV/AP prime-counting theorem.

theorem AnalyticNumberTheory.LargeSieve.standardPrimeAPPrefixMaxError_le_principal_character_bridge {N q : ℕ} (hq : 0 < q) : MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ discreteAbelAmplifierPrefixMax N * ((↑q.totient)⁻¹ * (principalLambdaPrefixMaxError N q + ∑ χ ∈ nonprincipalCharacters q, lambdaCharacterPrefixMaxAmplitude N q χ) + lambdaPrimePowerCorrectionPrefixMaxError N q) + (↑q.totient)⁻¹ * globalChebyshevToLiSourcePrefixMaxError N

Composition with the already-proved principal/nonprincipal character majorant. In particular the global/principal Chebyshev error remains visible and is not silently charged to the nonprincipal characters.