Richert 1969: Lemma 3 and the payment from ordinary Bombieri

Frozen source:

• references/richert-1969/richert-1969.pdf, PDF page 14, equations (3.24)--(3.25);
• the same PDF, pages 17--20, especially ordinary Bombieri (4.18) and the following Cauchy--Schwarz argument;
• references/richert-1969/VISION_TRANSCRIPTION.md, sections 7 and 9.

The source does not invoke a weighted Bombieri theorem as a black box. It applies Cauchy--Schwarz, uses Lemma 3 with h = 9 to pay the square of 3 ^ omega(d), and uses a pointwise d E*(N,d) envelope on the second factor. The theorem below records exactly that finite implication.

noncomputable def MathlibNt.SieveTheory.Richert1969.lemma3NineOmegaMass (S : Finset ℕ) : ℝ

The divisor weight in the square of Richert's 3 ^ omega(d) error sum.

Equations

• MathlibNt.SieveTheory.Richert1969.lemma3NineOmegaMass S = ∑ d ∈ S, 9 ^ d.primeFactors.card / ↑d

def MathlibNt.SieveTheory.Richert1969.threeOmegaErrorMass (S : Finset ℕ) (E : ℕ → ℝ) : ℝ

The weighted error sum that appears after the two sieve remainders are reindexed by their combined modulus.

Equations

• MathlibNt.SieveTheory.Richert1969.threeOmegaErrorMass S E = ∑ d ∈ S, 3 ^ d.primeFactors.card * E d

theorem MathlibNt.SieveTheory.Richert1969.lemma3NineOmegaMass_le_J9Mass (S : Finset ℕ) (Q : ℕ) (hS : S ⊆ Finset.range (Q + 1)) (hSquarefree : ∀ d ∈ S, Squarefree d) : lemma3NineOmegaMass S ≤ LiuWeight.liuPanPrimePowerJ9Mass Q

Richert's Lemma 3 at h = 9, specialized to a finite squarefree carrier: the required mass is dominated by the finite J₉ Euler-product mass.

theorem MathlibNt.SieveTheory.Richert1969.lemma3NineOmegaMass_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℕ), ∀ S ⊆ Finset.range (Q + 1), (∀ d ∈ S, Squarefree d) → lemma3NineOmegaMass S ≤ C * Real.log (↑Q + 2) ^ 9

The h = 9 case of Richert's Lemma 3 in the polylogarithmic form used after Cauchy--Schwarz. Its constant is independent of the carrier and cutoff.

theorem MathlibNt.SieveTheory.Richert1969.weightedError_sq_le_lemma3Mass_mul_ordinary (S : Finset ℕ) (w E : ℕ → ℝ) (X : ℝ) (hd : ∀ d ∈ S, 0 < d) (hE : ∀ d ∈ S, 0 ≤ E d) (henvelope : ∀ d ∈ S, ↑d * E d ≤ X) : (∑ d ∈ S, w d * E d) ^ 2 ≤ (∑ d ∈ S, w d ^ 2 / ↑d) * (X * ∑ d ∈ S, E d)

Finite Cauchy--Schwarz in the exact form used after (4.18).

sum E is the ordinary Bombieri mass. The pointwise estimate d * E d ≤ X turns the second Cauchy factor into X * sum E; the first factor is the h = 9 instance of Lemma 3.

theorem MathlibNt.SieveTheory.Richert1969.threeOmegaError_sq_le_of_ordinaryBombieri (S : Finset ℕ) (E : ℕ → ℝ) (X L B : ℝ) (hd : ∀ d ∈ S, 0 < d) (hE : ∀ d ∈ S, 0 ≤ E d) (hX : 0 ≤ X) (hL : 0 ≤ L) (henvelope : ∀ d ∈ S, ↑d * E d ≤ X) (hLemma3 : lemma3NineOmegaMass S ≤ L ^ 9) (hOrdinaryBombieri : ∑ d ∈ S, E d ≤ B) : threeOmegaErrorMass S E ^ 2 ≤ L ^ 9 * (X * B)

Richert's explicit payment: Lemma 3 at h = 9, ordinary Bombieri (4.18), and the elementary pointwise envelope imply the 3 ^ omega weighted error bound. No weighted Bombieri conclusion is assumed.

theorem MathlibNt.SieveTheory.Richert1969.threeOmegaError_sq_le_of_ordinaryBombieri_squarefree (S : Finset ℕ) (Q : ℕ) (E : ℕ → ℝ) (X B : ℝ) (hS : S ⊆ Finset.range (Q + 1)) (hSquarefree : ∀ d ∈ S, Squarefree d) (hE : ∀ d ∈ S, 0 ≤ E d) (hX : 0 ≤ X) (henvelope : ∀ d ∈ S, ↑d * E d ≤ X) (hOrdinaryBombieri : ∑ d ∈ S, E d ≤ B) : ∃ (C : ℝ), 0 < C ∧ threeOmegaErrorMass S E ^ 2 ≤ C * Real.log (↑Q + 2) ^ 9 * (X * B)

Richert's complete finite payment from Lemma 3 and an ordinary Bombieri mass, with no weighted Bombieri conclusion assumed. Squarefreeness and the cutoff discharge Lemma 3 through J₉; Cauchy--Schwarz pays the 3^ω weight.