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.

theorem MathlibNt.SieveTheory.Richert1969.exists_reciprocal_totient_le_richert_log_div : ∃ (C : ℝ), 0 < C ∧ ∀ (N m : ℕ), 2 ≤ N → 1 ≤ m → m ≤ N → 1 / ↑m.totient ≤ C * Real.log ↑N / ↑m

Mertens' product theorem pays the reciprocal totient in the pointwise m E*(N,m) estimate, uniformly for 1 ≤ m ≤ N.

theorem MathlibNt.SieveTheory.Richert1969.primesInAP_le_div_add_one (N m l : ℕ) (_hm : 0 < m) : BombieriVinogradov.primesInAP N m l ≤ N / m + 1

A residue class modulo m contains at most N / m + 1 integers through the endpoint N; primality can only decrease that count.

theorem MathlibNt.SieveTheory.Richert1969.modulus_mul_primesInAP_le (N m l : ℕ) (hm : 0 < m) : m * BombieriVinogradov.primesInAP N m l ≤ N + m

Multiplying the preceding residue-class count by its modulus costs at most one additional modulus.

noncomputable def MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant : ℝ

One fixed positive constant in the Mertens reciprocal-totient bound.

Equations

• MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant = Classical.choose MathlibNt.SieveTheory.Richert1969.exists_reciprocal_totient_le_richert_log_div

theorem MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant_pos : 0 < richertReciprocalTotientConstant

theorem MathlibNt.SieveTheory.Richert1969.reciprocal_totient_le_richertConstant_log_div {N m : ℕ} (hN : 2 ≤ N) (hm : 1 ≤ m) (hmN : m ≤ N) : 1 / ↑m.totient ≤ richertReciprocalTotientConstant * Real.log ↑N / ↑m

noncomputable def MathlibNt.SieveTheory.Richert1969.richert418PointwiseEnvelopeConstant : ℝ

The fixed coefficient in the elementary pointwise m E*(N,m) ≪ N(1 + log N) envelope.

Equations

• MathlibNt.SieveTheory.Richert1969.richert418PointwiseEnvelopeConstant = 2 + MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralUpperConstant 0 * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant / Real.log 2

theorem MathlibNt.SieveTheory.Richert1969.richert418PointwiseEnvelopeConstant_pos : 0 < richert418PointwiseEnvelopeConstant

theorem MathlibNt.SieveTheory.Richert1969.modulus_mul_primeAPPrefixMaxError_le {N m : ℕ} (hN : 2 ≤ N) (hm : 1 ≤ m) (hmN : m ≤ N) : ↑m * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m ≤ richert418PointwiseEnvelopeConstant * ↑N * (1 + Real.log ↑N)

Uniform pointwise envelope for Richert's exact nested maximum. It is the elementary second-factor input in the Cauchy step following (4.22).

theorem MathlibNt.SieveTheory.Richert1969.chenReducedCombinedModuli_le_liuSourceDEpsilon {N m : ℕ} {ε : ℝ} (hm : m ∈ chenReducedCombinedModuli N ε) : m ≤ LiuWeight.liuSourceDEpsilon N ε

The real combined-modulus bound lands in the floor-safe source cutoff. This is the exact integer form needed before invoking (4.18).

theorem MathlibNt.SieveTheory.Richert1969.eventually_chenReducedCombinedModuli_subset_panModulusCutoff (ε B : ℝ) (hε : 0 < ε) (hB : 0 ≤ B) : ∀ᶠ (N : ℕ) in Filter.atTop, chenReducedCombinedModuli N ε ⊆ Finset.Icc 1 (LiuWeight.panModulusCutoff N B)

For every positive level loss and nonnegative logarithmic cutoff exponent, Chen's exact combined moduli eventually lie in the modulus range of (4.18).

theorem MathlibNt.SieveTheory.Richert1969.eventually_sum_richertEStar_combined_le_of_ordinary418 (h418 : AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.Richert418BombieriVinogradov) (ε U : ℝ) (hε : 0 < ε) (hU : 0 < U) : ∃ (B : ℝ), 0 < B ∧ ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∑ m ∈ chenReducedCombinedModuli N ε, AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N m ≤ K * ↑N / Real.log ↑N ^ U

Quantified ordinary (4.18), specialized by finite subset monotonicity to Chen's exact combined-modulus carrier.

theorem MathlibNt.SieveTheory.Richert1969.chenReducedPairWeightedEStar_sq_le_of_ordinary418_floorSafe (N Q : ℕ) (ε B : ℝ) (hN : 2 ≤ N) (hε : 0 ≤ ε) (hsubset : chenReducedCombinedModuli N ε ⊆ Finset.Icc 1 Q) (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 * (richert418PointwiseEnvelopeConstant * ↑N * (1 + Real.log ↑N) * B)

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).

noncomputable def MathlibNt.SieveTheory.Richert1969.richertStandardPointwiseEnvelopeConstant : ℝ

The fixed pointwise-envelope coefficient after translating back from Richert's literal integral to the project's standard normalization.

Equations

• MathlibNt.SieveTheory.Richert1969.richertStandardPointwiseEnvelopeConstant = MathlibNt.SieveTheory.Richert1969.richert418PointwiseEnvelopeConstant + 2 / Real.log 2 * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant

theorem MathlibNt.SieveTheory.Richert1969.richertStandardPointwiseEnvelopeConstant_pos : 0 < richertStandardPointwiseEnvelopeConstant

theorem MathlibNt.SieveTheory.Richert1969.modulus_mul_standardPrimeAPMaxError_le_on_combined {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ chenReducedCombinedModuli N ε) (hε : 0 ≤ ε) : ↑m * BombieriVinogradov.standardPrimeAPMaxError N m ≤ richertStandardPointwiseEnvelopeConstant * ↑N * (1 + Real.log ↑N)

The explicit fixed normalization shift preserves the same N(1 + log N) pointwise envelope on every Chen combined modulus.

theorem MathlibNt.SieveTheory.Richert1969.chenReducedWeightedBVSum_le_combinedMass (N : ℕ) (ε : ℝ) : SwitchingPrinciple.jurkatRichertSourceReducedWeightedBVSum N ε ≤ threeOmegaErrorMass (chenReducedCombinedModuli N ε) (BombieriVinogradov.standardPrimeAPMaxError N)

The exact injective (q,d) ↦ qd reindexing pays the 3^ω(d) weight for the project's standard endpoint errors as well.

noncomputable def MathlibNt.SieveTheory.Richert1969.richertLemma3NineConstant : ℝ

One fixed positive constant in Richert's Lemma 3 payment at h = 9.

Equations

• MathlibNt.SieveTheory.Richert1969.richertLemma3NineConstant = Classical.choose MathlibNt.SieveTheory.Richert1969.lemma3NineOmegaMass_le_polylog

theorem MathlibNt.SieveTheory.Richert1969.richertLemma3NineConstant_pos : 0 < richertLemma3NineConstant

theorem MathlibNt.SieveTheory.Richert1969.lemma3NineOmegaMass_le_richertConstant (Q : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.range (Q + 1)) (hSquarefree : ∀ d ∈ S, Squarefree d) : lemma3NineOmegaMass S ≤ richertLemma3NineConstant * Real.log (↑Q + 2) ^ 9

theorem MathlibNt.SieveTheory.Richert1969.chenReducedWeightedBVSum_sq_le_of_ordinary (N Q : ℕ) (ε B : ℝ) (hN : 2 ≤ N) (hε : 0 ≤ ε) (hsubset : chenReducedCombinedModuli N ε ⊆ Finset.Icc 1 Q) (hOrdinary : ∑ m ∈ Finset.Icc 1 Q, BombieriVinogradov.standardPrimeAPPrefixMaxError N m ≤ B) : SwitchingPrinciple.jurkatRichertSourceReducedWeightedBVSum N ε ^ 2 ≤ richertLemma3NineConstant * Real.log (↑Q + 2) ^ 9 * (richertStandardPointwiseEnvelopeConstant * ↑N * (1 + Real.log ↑N) * B)

Standard endpoint-error version of the floor-safe finite payment. The ordinary input remains the unweighted prefix-maximal Bombieri mass.

theorem MathlibNt.SieveTheory.Richert1969.panModulusCutoff_le_endpoint (N : ℕ) (B : ℝ) (hN : 3 ≤ N) (hB : 0 ≤ B) : LiuWeight.panModulusCutoff N B ≤ N

Pan's floor cutoff is at most the endpoint once N ≥ 3 and the logarithmic exponent is nonnegative.

theorem MathlibNt.SieveTheory.Richert1969.chenWeightedBombieriVinogradov_of_standard (hBV : BombieriVinogradov.StandardBombieriVinogradov) : SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov

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.

theorem MathlibNt.SieveTheory.Richert1969.chenWeightedLowerBound_of_importedTheoremA_and_standardBombieri (hLowerTheoremA : SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hOrdinaryBombieri : BombieriVinogradov.StandardBombieriVinogradov) (hUpperTheoremA : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound

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.

structure MathlibNt.SieveTheory.Richert1969.ChenFacingSourceChainCertificate : Prop

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
• weightedObject (N : ℕ) : SwitchingPrinciple.jurkatRichertSourceWeightedCount N = ↑(SwitchingPrinciple.jurkatRichertSourceCandidates N).card - SwitchingPrinciple.jurkatRichertSourceMediumPrimeAggregate N / 2
• 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

theorem MathlibNt.SieveTheory.Richert1969.chenFacingSourceChainCertificate_of_importedTheoremA_and_standardBombieri (hLowerTheoremA : SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hOrdinaryBombieri : BombieriVinogradov.StandardBombieriVinogradov) (hUpperTheoremA : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) : ChenFacingSourceChainCertificate

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.