Richert 1969: the combined-modulus E-star adapter

Frozen source:

• references/richert-1969/richert-1969.pdf, PDF pages 10 and 17--20, equations (3.9)--(3.10), (4.18), and the Cauchy argument after (4.22);
• references/richert-1969/VISION_TRANSCRIPTION.md, sections 5, 7, and 9.

The source first replaces (q,d) by the injective combined modulus q*d. Ordinary Bombieri (4.18) controls Richert's prefix-maximal E* on that carrier. This file proves the exact finite reindexing and both directions of the fixed logarithmic-integral normalization comparison. It does not assume the divisor-weighted Bombieri conclusion.

noncomputable def MathlibNt.SieveTheory.Richert1969.richert418NormalizationShift (q : ℕ) : ℝ

The fixed positive shift between the project's standard prime-AP center and Richert's literal integral from 2 to x.

Equations

• MathlibNt.SieveTheory.Richert1969.richert418NormalizationShift q = 2 / Real.log 2 / ↑q.totient

theorem MathlibNt.SieveTheory.Richert1969.richert418NormalizationShift_nonneg {q : ℕ} (hq : 0 < q) : 0 ≤ richert418NormalizationShift q

theorem MathlibNt.SieveTheory.Richert1969.standardPrimeAPMaxError_le_richert_add (x q : ℕ) (hq : 0 < q) (hres : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty) : BombieriVinogradov.standardPrimeAPMaxError x q ≤ AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPResidueMaxError x q + richert418NormalizationShift q

Reverse normalization comparison: the project's endpoint maximum is at most Richert's residue maximum plus the explicit fixed shift.

theorem MathlibNt.SieveTheory.Richert1969.standardPrimeAPMaxError_le_richertEStar_add (N q : ℕ) (hN : 2 ≤ N) (hq : 0 < q) (hres : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty) : BombieriVinogradov.standardPrimeAPMaxError N q ≤ AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N q + richert418NormalizationShift q

Endpoint-to-prefix normalization on every positive combined modulus. The hypothesis 2 ≤ N is exactly the lower endpoint in Richert's E*.

noncomputable def MathlibNt.SieveTheory.Richert1969.chenReducedPairWeightedEStar (N : ℕ) (ε : ℝ) : ℝ

The 3^ω(d)-weighted Richert E* mass on Chen's exact reduced pair carrier, before reindexing by m = q*d.

Equations

• MathlibNt.SieveTheory.Richert1969.chenReducedPairWeightedEStar N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N with ¬q ∣ N, ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with d < MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε, 3 ^ d.primeFactors.card * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N (q * d)

theorem MathlibNt.SieveTheory.Richert1969.reducedWeightedBVSum_le_richertEStar_add_shift (N : ℕ) (ε : ℝ) (hN : 2 ≤ N) : SwitchingPrinciple.jurkatRichertSourceReducedWeightedBVSum N ε ≤ ∑ q ∈ SwitchingPrinciple.jurkatRichertSourceMediumPrimes N with ¬q ∣ N, ∑ d ∈ (SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with d < SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε, 3 ^ d.primeFactors.card * (AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N (q * d) + richert418NormalizationShift (q * d))

Exact normalization of the existing endpoint-error carrier against Richert's prefix-maximal E*, retaining the explicit fixed shift at every combined modulus.

noncomputable def MathlibNt.SieveTheory.Richert1969.chenReducedCombinedModuli (N : ℕ) (ε : ℝ) : Finset ℕ

The image of Chen's reduced (q,d) carrier under the combined-modulus map from Richert (3.9)--(3.10).

Equations

• MathlibNt.SieveTheory.Richert1969.chenReducedCombinedModuli N ε = {q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N | ¬q ∣ N}.biUnion fun (q : ℕ) => Finset.image (fun (d : ℕ) => q * d) ({d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors | d < MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε})

theorem MathlibNt.SieveTheory.Richert1969.chenReducedCombinedModulusFibres_pairwise (N : ℕ) (ε : ℝ) (q₁ : ℕ) : q₁ ∈ {q ∈ SwitchingPrinciple.jurkatRichertSourceMediumPrimes N | ¬q ∣ N} → ∀ q₂ ∈ {q ∈ SwitchingPrinciple.jurkatRichertSourceMediumPrimes N | ¬q ∣ N}, q₁ ≠ q₂ → Disjoint (Finset.image (fun (d : ℕ) => q₁ * d) ({d ∈ (SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors | d < SwitchingPrinciple.jurkatRichertSourceUpperLevel N q₁ ε})) (Finset.image (fun (d : ℕ) => q₂ * d) ({d ∈ (SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors | d < SwitchingPrinciple.jurkatRichertSourceUpperLevel N q₂ ε}))

Distinct reduced medium primes have disjoint combined-modulus fibres.

theorem MathlibNt.SieveTheory.Richert1969.sum_richertEStar_combined_eq_pairSum (N : ℕ) (ε : ℝ) : ∑ m ∈ chenReducedCombinedModuli N ε, AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m = ∑ q ∈ SwitchingPrinciple.jurkatRichertSourceMediumPrimes N with ¬q ∣ N, ∑ d ∈ (SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with d < SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε, AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N (q * d)

Exact (q,d) ↦ q*d reindexing of Richert's ordinary E* mass. Fibre uniqueness is proved on Chen's literal source carrier, so no multiplicity is discarded.

theorem MathlibNt.SieveTheory.Richert1969.chenReducedPairWeightedEStar_le_combinedMass (N : ℕ) (ε : ℝ) : chenReducedPairWeightedEStar N ε ≤ threeOmegaErrorMass (chenReducedCombinedModuli N ε) (AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N)

Reindexing also pays Richert's divisor weight: because d ∣ q*d, 3^ω(d) ≤ 3^ω(q*d), and injectivity prevents any repeated combined modulus.

theorem MathlibNt.SieveTheory.Richert1969.chenReducedCombinedModuli_cast_le {N m : ℕ} {ε : ℝ} (hm : m ∈ chenReducedCombinedModuli N ε) : ↑m ≤ ↑N ^ (1 / 2 - ε)

Every combined modulus lies in the literal real cutoff q*d ≤ N^(1/2-ε) supplied by the varying source level.

theorem MathlibNt.SieveTheory.Richert1969.sum_richertEStar_combined_le_initialRange (N Q : ℕ) (ε : ℝ) (hcut : ↑N ^ (1 / 2 - ε) ≤ ↑Q) : ∑ m ∈ chenReducedCombinedModuli N ε, AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m ≤ ∑ m ∈ Finset.Icc 1 Q, AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m

If the real Chen level lies below the integer (4.18) cutoff, ordinary Bombieri pays the exact combined-modulus E* mass by finite subset monotonicity.

theorem MathlibNt.SieveTheory.Richert1969.chenReducedPairWeightedEStar_sq_le_of_ordinary418 (N Q : ℕ) (ε X B : ℝ) (hcut : ↑N ^ (1 / 2 - ε) ≤ ↑Q) (hX : 0 ≤ X) (henvelope : ∀ m ∈ chenReducedCombinedModuli N ε, ↑m * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m ≤ X) (hOrdinary418 : ∑ m ∈ Finset.Icc 1 Q, AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m ≤ B) : ∃ (C : ℝ), 0 < C ∧ chenReducedPairWeightedEStar N ε ^ 2 ≤ C * Real.log (↑Q + 2) ^ 9 * (X * B)

Richert's actual finite Cauchy/Lemma 3 payment on Chen's combined moduli. The only distribution premise is the ordinary unweighted (4.18) mass on the initial modulus range.