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.
Richert's li x normalization in (4.18): the literal integral from 2
to x, with no added constant.
Equations
Instances For
Richert's ordinary prime-AP error E(x;q,l) from (4.18).
Equations
Instances For
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
Instances For
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
Instances For
The exact additive shift between Richert's literal integral and the project's domination-friendly Standard-BV normalization.
Changing from the project's Standard-BV normalization to Richert's literal
integral costs exactly one positive constant divided by phi(q).
Richert's exact nested maximum is bounded by the existing Standard-BV prefix maximum plus the explicit normalization shift.
Summed normalization comparison on an arbitrary initial modulus range.
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
Instances For
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.
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.