AnalyticNumberTheory.Sieve.LinearSieve

Linear sieve and Jurkat--Richert interfaces

The Jurkat--Richert theorem (1965) is a central tool for the lower bound on W(N) in Chen's theorem. It expresses upper and lower sieve bounds using functions F(s) and f(s).

The intended delay-differential description is:

• F(s) = 2e^γ / s on the initial range 2 ≤ s ≤ 4;
• f(s) = 0 for s ≤ 3;
• (s·F(s))' = f(s-1) for s ≥ 4;
• (s·f(s))' = F(s-1) for s ≥ 3, where γ is the Euler--Mascheroni constant.

The definitions below use explicit initial formulas, with F(2) = 1 by the first branch, and approximate extensions beyond their initial ranges. They do not implement the full delay-differential recursion. The module proves finite sieve bridges and fixed-parameter remainder interfaces, and records uniform main-term and lower-bound propositions with an implication between them.

References:

• Jurkat & Richert (1965), Acta Arith. 11, 217-240
• Halberstam & Richert, "Sieve Methods" (1974), Ch. 8
• Liu, Z. (2022), arXiv:2203.07871, §III

0. Finite lower-bound sieve interface

def AnalyticNumberTheory.Sieve.IsLowerMoebius (muMinus : ℕ → ℝ) : Prop

A sequence of coefficients is lower Möbius when its divisor sums lie below the coprimality indicator. This is the exact finite dual of Mathlib's BoundingSieve.IsUpperMoebius.

Equations

• AnalyticNumberTheory.Sieve.IsLowerMoebius muMinus = ∀ (n : ℕ), ∑ d ∈ n.divisors, muMinus d ≤ if n = 1 then 1 else 0

theorem AnalyticNumberTheory.Sieve.sum_of_lowerMoebius_le_siftedSum {S : BoundingSieve} (muMinus : ℕ → ℝ) (hmu : IsLowerMoebius muMinus) : ∑ d ∈ S.prodPrimes.divisors, muMinus d * BoundingSieve.multSum d ≤ BoundingSieve.siftedSum

A lower Möbius sequence gives a lower bound for the sifted sum before any asymptotic estimate is introduced.

theorem AnalyticNumberTheory.Sieve.mainSum_sub_errSum_le_siftedSum_of_lowerMoebius {S : BoundingSieve} (muMinus : ℕ → ℝ) (hmu : IsLowerMoebius muMinus) : S.totalMass * BoundingSieve.mainSum muMinus - BoundingSieve.errSum muMinus ≤ BoundingSieve.siftedSum

Explicit-error lower sieve inequality. Unlike the historical pointwise interfaces, the loss is the concrete finite quantity errSum muMinus.

1. Euler--Mascheroni constant

@[reducible, inline]

noncomputable abbrev AnalyticNumberTheory.Sieve.eulerMascheroni : ℝ

The Euler--Mascheroni constant γ ≈ 0.5772..., defined as the limit of the difference between the harmonic sum and the logarithm.

Equations

• AnalyticNumberTheory.Sieve.eulerMascheroni = Real.eulerMascheroniConstant

2. Sieve functions F(s) and f(s)

noncomputable def AnalyticNumberTheory.Sieve.sieveFunctionF (s : ℝ) : ℝ

Piecewise upper sieve function F(s):

• s ≤ 2: F(s) = 1, the trivial branch;
• 2 < s ≤ 4: F(s) = 2e^γ / s;
• s > 4: an approximate extension is used here.

The full extension would require the delay-differential recursion (s·F(s))' = f(s-1); it is not defined by that recursion here.

Equations

• AnalyticNumberTheory.Sieve.sieveFunctionF s = if s ≤ 2 then 1 else if s ≤ 4 then 2 * Real.exp AnalyticNumberTheory.Sieve.eulerMascheroni / s else 2 * Real.exp AnalyticNumberTheory.Sieve.eulerMascheroni / s * (1 + 1 / s)

noncomputable def AnalyticNumberTheory.Sieve.sieveFunctionf (s : ℝ) : ℝ

Lower sieve function f(s) of the Jurkat--Richert linear sieve.

• s ≤ 3: f(s) = 0
• 3 < s ≤ 5: f(s) = 2e^γ · log((s - 1) / 2) / s
• s > 5: placeholder (the Buchstab delay recursion is not yet formalized)

The formula on (3, 5] is the standard Jurkat--Richert value: with F(s) = 2e^γ / s on [2, 4], the delay equation (s·f(s))' = F(s - 1) and the boundary value f(3) = 0 give f(s) = (2e^γ / s) · log((s - 1) / 2) for 3 ≤ s ≤ 5. This is the value used at the Chen sieve ratio s = D/z ≈ 5.

For s > 5 the recursion must continue through the Buchstab-type F; the expression below is only a placeholder and must not be used to justify Chen's classical constants.

Equations

• AnalyticNumberTheory.Sieve.sieveFunctionf s = if s ≤ 3 then 0 else if s ≤ 5 then 2 * Real.exp AnalyticNumberTheory.Sieve.eulerMascheroni / s * Real.log ((s - 1) / 2) else 2 * Real.exp AnalyticNumberTheory.Sieve.eulerMascheroni / s * Real.log ((s - 1) / 2) * (1 + 1 / s)

3. Basic properties of the sieve functions

theorem AnalyticNumberTheory.Sieve.sieveF_pos_on_2_4 {s : ℝ} (_hs : 2 ≤ s) (hs' : s ≤ 4) : 0 < sieveFunctionF s

F(s) is positive on [2,4].

theorem AnalyticNumberTheory.Sieve.sievef_pos_on_3_5 {s : ℝ} (hs : 3 < s) (hs' : s ≤ 5) : 0 < sieveFunctionf s

f(s) is positive on (3,5].

theorem AnalyticNumberTheory.Sieve.sievef_le_sieveF {s : ℝ} (hs : 2 ≤ s) (hs' : s ≤ 4) : sieveFunctionf s ≤ sieveFunctionF s

f(s) ≤ F(s): the lower sieve function does not exceed the upper one on [2,4].

• For s ≤ 2, F = 1 and f = 0.
• For 2 < s ≤ 3, F = 2e^γ/s > 0 and f = 0.
• For 3 < s ≤ 4, F = 2e^γ/s and f = 2e^γ/s·log((s-1)/2). By log_le_sub_one, log((s-1)/2) ≤ (s-1)/2 - 1 ≤ 1 since s ≤ 4, so f ≤ F.

The classical range s > 4 requires the full Buchstab-type delay-differential analysis.

4. Sieve setup via Mathlib.BoundingSieve

structure AnalyticNumberTheory.Sieve.SieveProblemextends BoundingSieve : Type

Sieve problem for Chen's theorem: extend mathlib's BoundingSieve with a sifting level z and distribution level D.

The correspondence with classical notation is:

• support: A, the set to sift, for example {N-p : p is prime};
• totalMass: X, an approximation to |A|, for example N/log N;
• nu: the multiplicative density ν, an ArithmeticFunction ℝ;
• weights: identically 1 in the unweighted counting specialization;
• prodPrimes: the product of primes below z;
• siftedSum: mathlib's inherited sum of weights over elements coprime to prodPrimes.

Additional fields specify z (removing multiples of primes below z), D (the range of controlled remainders), and prodPrimes_eq (the required prime-product representation).

• support : Finset ℕ
• prodPrimes : ℕ
• prodPrimes_squarefree : Squarefree self.prodPrimes
• weights : ℕ → ℝ
• weights_nonneg (n : ℕ) : 0 ≤ self.weights n
• totalMass : ℝ
• nu : ArithmeticFunction ℝ
• nu_mult : self.nu.IsMultiplicative
• nu_pos_of_prime (p : ℕ) : Nat.Prime p → p ∣ self.prodPrimes → 0 < self.nu p
• nu_lt_one_of_prime (p : ℕ) : Nat.Prime p → p ∣ self.prodPrimes → self.nu p < 1
• z : ℝ

  Sifting level z: remove multiples of primes below z.

• hz_pos : 0 < self.z
• D : ℝ

  Distribution level D: the range of controlled remainders, classically supplied by Bombieri--Vinogradov.

• hD_pos : 0 < self.D
• prodPrimes_eq : self.prodPrimes = (Finset.filter Nat.Prime (Finset.range ⌈self.z⌉₊)).prod id

  prodPrimes is the product of primes below z.

theorem AnalyticNumberTheory.Sieve.siftedSum_eq_filter (SP : SieveProblem) (hweights : ∀ (n : ℕ), SP.weights n = 1) : BoundingSieve.siftedSum = ∑ x ∈ SP.support with ∀ (p : ℕ), Nat.Prime p → ↑p < SP.z → ¬p ∣ x, 1

Counting bridge: mathlib's siftedSum = ∑ d ∈ support, if Coprime prodPrimes d then weights d else 0 equals |{a ∈ A : ∀ p prime, p < z → ¬ p ∣ a}| when prodPrimes is the product of primes below z and weights = 1 (the hypothesis hweights).

noncomputable def AnalyticNumberTheory.Sieve.sieveProduct (SP : SieveProblem) : ℝ

Sieve product V(z) = Π_{p < z} (1 - ν(p)), the product appearing in the Jurkat--Richert main term X·V(z)·f(s).

Mathlib's selbergTerms d = ν(d)·Π_{p|d} (1 - ν(p))⁻¹. At d = prodPrimes, the product of primes below z, this gives selbergTerms prodPrimes = ν(prodPrimes)/V(z), hence V(z) = ν(prodPrimes)/selbergTerms(prodPrimes). Mathlib's density is normalized as ν(p) = ω(p)/p, so 1 - ν(p) = 1 - ω(p)/p is the standard sieve factor.

Equations

• AnalyticNumberTheory.Sieve.sieveProduct SP = ∏ p ∈ Finset.range ⌈SP.z⌉₊ with Nat.Prime p, (1 - SP.nu p)

theorem AnalyticNumberTheory.Sieve.sieveProduct_eq_prod_one_sub_nu (SP : SieveProblem) : sieveProduct SP = ∏ p ∈ SP.prodPrimes.primeFactors, (1 - SP.nu p)

Product bridge: sieveProduct = Π_{p | prodPrimes} (1 - ν(p)). By prodPrimes_eq, for prime p, divisibility by prodPrimes is equivalent to p < z.

theorem AnalyticNumberTheory.Sieve.sieveProduct_mul_selbergTerms_eq_nu (SP : SieveProblem) : sieveProduct SP * BoundingSieve.selbergTerms SP.prodPrimes = SP.nu SP.prodPrimes

Selberg-term bridge: sieveProduct · selbergTerms(prodPrimes) = ν(prodPrimes). By mathlib's selbergTerms_apply, selbergTerms d = ν(d)·Π_{p|d} (1 - ν(p))⁻¹. For d = prodPrimes, this is ν(prodPrimes)·Π_{p|prodPrimes} (1 - ν(p))⁻¹ = ν(prodPrimes)/sieveProduct; multiplying gives the identity.

theorem AnalyticNumberTheory.Sieve.sieveProduct_eq_nu_div_selbergTerms (SP : SieveProblem) : sieveProduct SP = SP.nu SP.prodPrimes / BoundingSieve.selbergTerms SP.prodPrimes

Quotient bridge: sieveProduct = ν(prodPrimes)/selbergTerms(prodPrimes).

theorem AnalyticNumberTheory.Sieve.distribution_condition (SP : SieveProblem) (d : ℕ) (_hd : ↑d ≤ SP.D) (_hd_pos : 1 ≤ d) : BoundingSieve.multSum d = SP.nu d * SP.totalMass + BoundingSieve.rem d

Distribution identity: for d ≤ D, the counting specialization is |{a ∈ A : d | a}| = ν(d)·X + R_d. This is mathlib's multSum_eq_main_err, multSum d = nu d * totalMass + rem d. The remainder rem d is R_d; the distribution level describes the range where it should be negligible, but this identity alone gives no remainder estimate.

5. Fixed-parameter Jurkat--Richert-shaped bounds

theorem AnalyticNumberTheory.Sieve.jurkat_richert_upper_bound (SP : SieveProblem) (_hs : 2 ≤ SP.D / SP.z) : ∃ (C_error : ℝ), BoundingSieve.siftedSum ≤ SP.totalMass * sieveProduct SP * sieveFunctionF (SP.D / SP.z) + C_error

Upper-bound remainder interface. The classical Jurkat--Richert upper bound has the form S(A,z) ≤ X·V(z)·(F(s) + O(η)) + Σ_{d ≤ D} |R_d|. Mathlib's siftedSum_le_mainSum_errSum_of_upperMoebius gives siftedSum ≤ totalMass·mainSum(μ⁺) + errSum(μ⁺). The analytic theorem further estimates mainSum(μ⁺) ≤ V(z)·F(s) and errSum ≤ Σ |R_d|. These are ingredients for the upper bound on Ω in Chen's theorem.

The present interface only asks for an unspecified additive error for a single SP; the absolute difference of the two sides supplies it. It is not a uniform Jurkat--Richert estimate, which must relate C_error to explicit bounds on SP.rem.

theorem AnalyticNumberTheory.Sieve.jurkat_richert_lower_bound (SP : SieveProblem) (_hs : 3 < SP.D / SP.z) : ∃ (C_error : ℝ), BoundingSieve.siftedSum ≥ SP.totalMass * sieveProduct SP * sieveFunctionf (SP.D / SP.z) - C_error

Lower-bound remainder interface. The classical Jurkat--Richert lower bound has the form S(A,z) ≥ X·V(z)·(f(s) - O(η)) - Σ_{d ≤ D} |R_d|. It is a theoretical input to the Chen estimate W(N) ≥ 2.6408 𝔖(N) N/log²N.

Here the quantifiers only assert an additive remainder for each individual SP; the uniform analytic lower bound is a separate input.

5.5 Uniform Jurkat--Richert lower-bound propositions

noncomputable def AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (S : BoundingSieve) : ℝ

Standard sieve product over the prime factors of prodPrimes: V_S = ∏_{p | prodPrimes} (1 - ν(p)). For a classical SieveProblem, where prodPrimes is the product of primes below z, this equals sieveProduct (sieveProduct_eq_sieveProductPrimeFactors). For the modified Chen sieve, prodPrimes already excludes 2 and the prime divisors of N, so this definition applies directly without requiring the representation through SieveProblem.z.

Equations

• AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S = ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p)

theorem AnalyticNumberTheory.Sieve.sieveProduct_eq_sieveProductPrimeFactors (SP : SieveProblem) : sieveProduct SP = sieveProductPrimeFactors SP.toBoundingSieve

The two sieve-product definitions agree for a classical SieveProblem.

theorem AnalyticNumberTheory.Sieve.errSum_le_of_abs_le_one {S : BoundingSieve} {mu : ℕ → ℝ} (h : ∀ (d : ℕ), |mu d| ≤ 1) : BoundingSieve.errSum mu ≤ BoundingSieve.errSum fun (x : ℕ) => 1

If |μ(d)| ≤ 1, then errSum μ ≤ errSum 1. This replaces errSum(μ⁻) in a uniform lower-bound argument by the explicit errSum(1) = Σ_{d | prodPrimes} |rem d|, corresponding to the classical Σ_{d ≤ D} |R_d|.

theorem AnalyticNumberTheory.Sieve.siftedSum_lower_bound_of_mainTerm {S : BoundingSieve} {fs : ℝ → ℝ} {t η : ℝ} {muMinus : ℕ → ℝ} (hmass : 0 ≤ S.totalMass) (hmu : IsLowerMoebius muMinus) (hbnd : ∀ (d : ℕ), |muMinus d| ≤ 1) (hmain : sieveProductPrimeFactors S * (fs t - η) ≤ BoundingSieve.mainSum muMinus) : (S.totalMass * sieveProductPrimeFactors S * (fs t - η) - BoundingSieve.errSum fun (x : ℕ) => 1) ≤ BoundingSieve.siftedSum

Finite lower-bound bridge: given a lower Moebius sequence muMinus with coefficients bounded in absolute value by 1, a main-term estimate V·(fs(t) - η) ≤ mainSum(μ⁻), and nonnegative total mass, one obtains X·V·(fs(t) - η) - errSum(1) ≤ siftedSum. Combine mainSum_sub_errSum_le_siftedSum_of_lowerMoebius with errSum_le_of_abs_le_one. Classically this corresponds to S(A,z) ≥ X·V(z)·(f(s) - O(η)) - Σ_{d ≤ D} |R_d|.

def AnalyticNumberTheory.Sieve.UniformJurkatRichertMainTerm (SP : ℕ → BoundingSieve) (zN DN : ℕ → ℝ) (fs : ℝ → ℝ) : Prop

Uniform main-term lower-bound proposition. There exist N₀ and η₀ > 0 such that for every even N ≥ N₀ there is a lower Moebius sequence muMinus, bounded in absolute value by 1, satisfying mainSum(μ⁻) ≥ V_N·(fs(D_N/z_N) - η₀). Here V_N = ∏_{p | prodPrimes_N} (1 - ν_N(p)) and fs is the chosen lower sieve function.

The constants N₀ and η₀ precede ∀ N and cannot depend on N. This records an additive-loss version of the classical estimate mainSum(μ⁻) ≥ V(z)·f(s)·(1 - O(η)). The API uses the ratio D_N/z_N as its function argument; identifying that argument with the classical logarithmic sieve ratio log D/log z ≈ 5 requires a compatible choice of parameters.

Equations

• AnalyticNumberTheory.Sieve.UniformJurkatRichertMainTerm SP zN DN fs = ∃ (N₀ : ℕ) (η₀ : ℝ), 0 < η₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (muMinus : ℕ → ℝ), AnalyticNumberTheory.Sieve.IsLowerMoebius muMinus ∧ (∀ (d : ℕ), |muMinus d| ≤ 1) ∧ AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (SP N) * (fs (DN N / zN N) - η₀) ≤ BoundingSieve.mainSum muMinus

def AnalyticNumberTheory.Sieve.UniformJurkatRichertLowerBound (SP : ℕ → BoundingSieve) (zN DN : ℕ → ℝ) (fs : ℝ → ℝ) : Prop

Uniform sieve lower-bound proposition. The classical Halberstam--Richert/Chen form is S(A,z) ≥ X·V(z)·(f(s) - O(η)) - Σ_{d ≤ D} |R_d| uniformly for all sufficiently large even N. The finite formulation here asks for N₀ and η₀ > 0 such that, for each even N ≥ N₀, there is a lower Moebius sequence muMinus bounded in absolute value by 1, with siftedSum ≥ X_N·V_N·(fs(D_N/z_N) - η₀) - errSum(1). The explicit divisor error is errSum(1) = Σ_{d | prodPrimes_N} |rem_N d|.

Quantifier order is essential: N₀ and η₀ precede ∀ N, unlike a fixed-parameter remainder interface (see CHEN_PROOF_ATLAS). The implication from UniformJurkatRichertMainTerm uses siftedSum_lower_bound_of_mainTerm; see UniformJurkatRichertLowerBound_of_uniformMainTerm.

Equations

• AnalyticNumberTheory.Sieve.UniformJurkatRichertLowerBound SP zN DN fs = ∃ (N₀ : ℕ) (η₀ : ℝ), 0 < η₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (muMinus : ℕ → ℝ), AnalyticNumberTheory.Sieve.IsLowerMoebius muMinus ∧ (∀ (d : ℕ), |muMinus d| ≤ 1) ∧ ((SP N).totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (SP N) * (fs (DN N / zN N) - η₀) - BoundingSieve.errSum fun (x : ℕ) => 1) ≤ BoundingSieve.siftedSum

theorem AnalyticNumberTheory.Sieve.UniformJurkatRichertLowerBound_of_uniformMainTerm (SP : ℕ → BoundingSieve) (zN DN : ℕ → ℝ) (fs : ℝ → ℝ) (hmass : ∀ (N : ℕ), 0 ≤ (SP N).totalMass) (hmain : UniformJurkatRichertMainTerm SP zN DN fs) : UniformJurkatRichertLowerBound SP zN DN fs

A uniform main-term estimate and nonnegative total mass imply the uniform sieve lower bound.

6. Application in Chen's theorem

6.5 Chen's key inequality

The definitions of W(N) and Ω(N) and the key inequality belong to SwitchingPrinciple.lean (chenW, chenOmega, chen_key_inequality). The deduction uses explicit uniform analytic and counting inputs. The fixed-parameter jurkat_richert_lower_bound here does not by itself supply those inputs. In particular, replacing both counts by zero would make W(N) - Ω(N)/2 > 0 false.

7. Scope and dependencies