Richert 1969: specialization of ordinary (4.18) to Chen's weighted remainder #
Frozen source:
references/richert-1969/richert-1969.pdf, PDF pages 17--20, equation (4.18) and the Cauchy--Schwarz argument after (4.22);references/richert-1969/VISION_TRANSCRIPTION.md, sections 7 and 9.
This module specializes the quantified ordinary prefix-maximal Bombieri--Vinogradov estimate to Chen's combined moduli. The cutoff, pointwise envelope, Lemma 3 payment, and logarithmic-integral normalization shift are all discharged here. No weighted Bombieri theorem is assumed.
Mertens' product theorem pays the reciprocal totient in the pointwise
m E*(N,m) estimate, uniformly for 1 ≤ m ≤ N.
A residue class modulo m contains at most N / m + 1 integers through
the endpoint N; primality can only decrease that count.
Multiplying the preceding residue-class count by its modulus costs at most one additional modulus.
One fixed positive constant in the Mertens reciprocal-totient bound.
Equations
Instances For
The fixed coefficient in the elementary pointwise
m E*(N,m) ≪ N(1 + log N) envelope.
Equations
Instances For
Uniform pointwise envelope for Richert's exact nested maximum. It is the elementary second-factor input in the Cauchy step following (4.22).
The real combined-modulus bound lands in the floor-safe source cutoff. This is the exact integer form needed before invoking (4.18).
For every positive level loss and nonnegative logarithmic cutoff exponent, Chen's exact combined moduli eventually lie in the modulus range of (4.18).
Quantified ordinary (4.18), specialized by finite subset monotonicity to Chen's exact combined-modulus carrier.
Floor-safe form of Richert's Cauchy/Lemma 3 payment on Chen's exact combined moduli. Its only distribution premise is the ordinary unweighted initial-range mass from (4.18).
The fixed pointwise-envelope coefficient after translating back from Richert's literal integral to the project's standard normalization.
Equations
Instances For
The explicit fixed normalization shift preserves the same
N(1 + log N) pointwise envelope on every Chen combined modulus.
The exact injective (q,d) ↦ qd reindexing pays the 3^ω(d) weight for
the project's standard endpoint errors as well.
One fixed positive constant in Richert's Lemma 3 payment at h = 9.
Equations
Instances For
Standard endpoint-error version of the floor-safe finite payment. The ordinary input remains the unweighted prefix-maximal Bombieri mass.
Pan's floor cutoff is at most the endpoint once N ≥ 3 and the
logarithmic exponent is nonnegative.
Ordinary Bombieri--Vinogradov pays Chen's exact 3^ω-weighted
varying-level remainder. The proof uses the quantified exponent
U = 2A + 10: nine logarithms are Richert Lemma 3 and one is the pointwise
m E envelope.
Chen-facing Richert source chain with Theorem A honestly imported and the
weighted varying-level error derived from ordinary Bombieri--Vinogradov
(4.18). The lower object, conditioned upper sieves, squareful correction,
and Stieltjes prime integral are assembled by the source-faithful Theorem 1
endpoint.
A single certificate carrying every literal Richert source stage used for
the Chen-facing specialization. The finite Theorem 1 and (A4) fields record
their exact conditional statements; the analytic endpoint retains Theorem A
as an imported dependency.
- theoremOneFinite (A : Finset ℕ) (X : ℝ) (K : ℕ) (v u lambda : ℝ) : 0 ≤ lambda → (∀ p ∈ theoremOneWeightedPrimes X K u v, 0 ≤ theoremOnePrimeWeight X u p) → ↑(lowerCarrier A (theoremOneSiftingProduct X K v)).card - squarefulCorrection A (theoremOneWeightedPrimes X K u v) (theoremOneSiftingProduct X K v) - lambda * primeConditionedUpperAggregate A (theoremOneWeightedPrimes X K u v) (theoremOneSiftingProduct X K v) (theoremOnePrimeWeight X u) ≤ theoremOneWeightedLowerObject A X K v u lambda
- lowerS (N : ℕ) : BoundingSieve.siftedSum = ↑(SwitchingPrinciple.jurkatRichertSourceCandidates N).card
- conditionedUpperS (N p : ℕ) : BoundingSieve.siftedSum = ↑{q ∈ SwitchingPrinciple.jurkatRichertSourceCandidates N | p ∣ N - q}.card
- squarefulA4 (A : Finset ℕ) (X : ℝ) (K : ℕ) (v u A4 : ℝ) : SquarefulA4On A (theoremOneWeightedPrimes X K u v) X A4 → squarefulCorrection A (theoremOneWeightedPrimes X K u v) (theoremOneSiftingProduct X K v) ≤ ∑ p ∈ theoremOneWeightedPrimes X K u v, A4 * (X * Real.log X / ↑p ^ 2 + 1)
- stieltjesPrimeIntegral : SwitchingPrinciple.ChenJurkatRichertVaryingQPrimeSumAsymptotic
- weightedBombieri : SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov
- weightedLowerBound : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound
Instances For
Complete source-chain certificate from lower/upper Theorem A and ordinary
Bombieri--Vinogradov. In particular, the 3^ω statement is a conclusion,
not an additional premise.