Richert (4.18) normalization and a modern large-sieve producer

Richert's 1969 paper defines

E*(N,q) = max_{2 <= x <= N} max_{(l,q)=1} |pi(x;q,l) - li(x)/phi(q)|

and cites Bombieri's Theorem 4 for its mean-value estimate. This module formalizes that exact displayed normalization from Richert.

The recovered Bombieri original was inspected separately. Its Theorem 4 is stated for the maximal von-Mangoldt error psi(z;q,a) - z / phi(q), not directly for Richert's prime-counting error. Thus the declarations below are deliberately labelled as Richert's partial-summation normalization rather than a verbatim Bombieri statement.

The final theorem is a modern replacement producer. It uses the project's large-sieve/Vaughan chain and retains only its genuine low-conductor nonprincipal primitive Siegel--Walfisz input.

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.logarithmicIntegral (x : ℝ) : ℝ

Richert's li x normalization in (4.18): the literal integral from 2 to x, with no added constant.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.logarithmicIntegral x = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral 0 x

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPError (x q l : ℕ) : ℝ

Richert's ordinary prime-AP error E(x;q,l) from (4.18).

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPError x q l = ↑(MathlibNt.SieveTheory.BombieriVinogradov.primesInAP x q l) - AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.logarithmicIntegral ↑x / ↑q.totient

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError (x q : ℕ) : ℝ

The inner maximum in Richert's E*, over canonical reduced residues. The inserted zero makes the definition total at q = 0; for every modulus in (4.18), the absolute-value family is nonempty and nonnegative.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError x q = (insert 0 (Finset.image (fun (l : ℕ) => |AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPError x q l|) (AnalyticNumberTheory.Sieve.unitResidues q))).max' ⋯

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

Richert's exact outer maximum in (4.18), over integer endpoints 2 <= x <= N. The inserted zero makes the definition total when N < 2.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N q = (insert 0 (Finset.image (fun (x : ℕ) => AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError x q) (Finset.Icc 2 N))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.abs_primeAPError_le_residueMax {x q l : ℕ} (hl : l ∈ Sieve.unitResidues q) : |primeAPError x q l| ≤ primeAPResidueMaxError x q

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError_nonneg (x q : ℕ) : 0 ≤ primeAPResidueMaxError x q

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError_le_prefixMax {N x q : ℕ} (hx : x ∈ Finset.Icc 2 N) : primeAPResidueMaxError x q ≤ primeAPPrefixMaxError N q

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError_nonneg (N q : ℕ) : 0 ≤ primeAPPrefixMaxError N q

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPError_eq_standard_add (x q l : ℕ) : primeAPError x q l = MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError x q l + 2 / Real.log 2 / ↑q.totient

The exact additive shift between Richert's literal integral and the project's domination-friendly Standard-BV normalization.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError_le_standard_add (x q : ℕ) (hq : 1 ≤ q) : primeAPResidueMaxError x q ≤ MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError x q + 2 / Real.log 2 / ↑q.totient

Changing from the project's Standard-BV normalization to Richert's literal integral costs exactly one positive constant divided by phi(q).

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError_le_standard_add (N q : ℕ) (hq : 1 ≤ q) : primeAPPrefixMaxError N q ≤ MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q + 2 / Real.log 2 / ↑q.totient

Richert's exact nested maximum is bounded by the existing Standard-BV prefix maximum plus the explicit normalization shift.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.sum_primeAPPrefixMaxError_le_standard_add (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, primeAPPrefixMaxError N q ≤ ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q + ↑Q * (2 / Real.log 2)

Summed normalization comparison on an arbitrary initial modulus range.

def AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.Richert418BombieriVinogradov : Prop

The exact proposition displayed as Richert (4.18), with the Vinogradov symbol expanded into an explicit positive multiplicative constant.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.Richert418BombieriVinogradov = ∀ (U : ℝ), 0 < U → ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N C), AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N q ≤ K * ↑N / Real.log ↑N ^ U

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.richert418_of_standardBombieriVinogradov (hBV : MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov) : Richert418BombieriVinogradov

Normalization adapter from the project's Standard-BV endpoint to the exact Richert (4.18) statement. The exponent is increased by one to remain positive; the smaller modulus range and the fixed li shift are paid explicitly.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.richert418_of_nonprincipalPrimitivePsi (hSW : NonprincipalPrimitivePsiSiegelWalfiszSource) : Richert418BombieriVinogradov

Modern large-sieve producer for Richert's exact (4.18) endpoint.

This is not presented as a transcription of Bombieri 1965. Its sole hypothesis is the pointwise nonprincipal primitive Siegel--Walfisz input; the high-conductor Vaughan and large-sieve work is supplied by the checked modern producer chain.