Elementary sieve applications and remainder interfaces #
Legacy sieve functions, the weighted sieve problem, counting and product identities, and fixed-parameter remainder interfaces.
1. The Euler-Mascheroni constant #
The Euler-Mascheroni constant γ ≈ 0.5772...
It is defined as the limit of the difference between the harmonic partial sums and the logarithm.
Instances For
2. The sieve functions F(s) and f(s) #
Legacy placeholder for an upper sieve function.
- s ≤ 2: F(s) = 1 (the trivial-bound branch);
- 2 < s ≤ 4: F(s) = 2e^γ / s;
- s > 4: a placeholder approximation rather than the recursion from the differential-delay equation (s·F(s))' = f(s-1).
Only the indicated explicit branch is implemented; extending the intended sieve function requires recursion. This is not the canonical dimension-one function used by the generic Rosser density interfaces.
Equations
Instances For
A nonstandard working normalization for a lower sieve function.
- s ≤ 3: f(s) = 0
- 3 < s ≤ 5: a local
log (s / 2)surrogate - s > 5: a further placeholder approximation
This is not claimed to be the standard Jurkat--Richert/Buchstab lower sieve function (whose normalization and differential-delay recursion must be formalized separately). It is used only in the fixed-parameter working interfaces below and must not be used to justify Chen's classical constants.
Equations
Instances For
3. Basic properties of the sieve functions #
F(s) is positive on [2, 4].
f(s) is positive on (3, 5].
f(s) ≤ F(s): the lower function does not exceed the upper function.
For s ∈ [2, 4], this follows by cases:
- s ≤ 2: F = 1, f = 0, and 0 ≤ 1.
- 2 < s ≤ 3: F = 2e^γ/s > 0 and f = 0.
- 3 < s ≤ 4: F = 2e^γ/s, f = 2e^γ/s·log(s/2).
By
log_le_sub_one, log(s/2) ≤ s/2-1 ≤ 1 since s ≤ 4, so f ≤ F.
For the intended sieve functions beyond s = 4, a full analysis of the Buchstab-type differential-delay recursion is required.
4. Sieve setup (aligned with Mathlib's BoundingSieve) #
Sieve problem for Chen's theorem: extend Mathlib's BoundingSieve
with a sifting level z and a level of distribution D.
Correspondence with Mathlib's BoundingSieve:
support← A, the set to be sifted, such as {N - p : p prime};totalMass← X, an approximation to |A|, such as N / log N;nu← ν, a multiplicative density function of typeArithmeticFunction ℝ;weights← the constant 1 in the counting-sieve specialization;prodPrimes← the product of primes < z, below the sifting level;siftedSum← Mathlib's definition, summing weights over d coprime to prodPrimes.
Additional fields for the Jurkat-Richert setup:
z: the sifting level, removing multiples of primes < z;D: the level of distribution, describing the range of controlled remainders;prodPrimes_eq: prodPrimes is the product of primes < z. The structure itself retains general weights; counting applications imposeweights = 1separately.
- prodPrimes : ℕ
- nu_mult : self.nu.IsMultiplicative
- z : ℝ
Sifting level z: remove multiples of primes < z.
- D : ℝ
Level of distribution D: the range of controlled remainders, supplied in applications by Bombieri-Vinogradov estimates.
prodPrimes is the product of primes < z.
Instances For
Bridge lemma: Mathlib's siftedSum agrees with the sifted count.
Mathlib: siftedSum = ∑ d ∈ support, if Coprime prodPrimes d then weights d else 0
Counting formulation: |{a ∈ A : ∀ p prime, p < z → ¬ p ∣ a}|
The two coincide when prodPrimes is the product of primes < z and
weights = 1, as assumed by hweights.
Sieve product V(z) = Π_{p < z} (1 - ν(p)).
This is a factor in the Jurkat-Richert main term X · V(z) · f(s).
Relation to Mathlib's selbergTerms:
selbergTerms d = ν(d) · Π_{p|d} (1 - ν(p))⁻¹.
For d = prodPrimes, the product of primes < z:
selbergTerms prodPrimes = ν(prodPrimes) / V(z)
and hence V(z) = ν(prodPrimes) / selbergTerms(prodPrimes).
Mathlib's density corresponds to ν(p) = ω(p)/p in classical notation,
so 1 - ν(p) = 1 - ω(p)/p is the standard sieve-density factor.
Equations
- MathlibNt.SieveTheory.LinearSieve.sieveProduct SP = ∏ p ∈ Finset.range ⌈SP.z⌉₊ with Nat.Prime p, (1 - SP.nu p)
Instances For
Bridge lemma 1: sieveProduct equals Π_{p | prodPrimes} (1 - ν(p)).
By prodPrimes_eq, prodPrimes is the product of primes < z.
Thus, for a prime p, p | prodPrimes if and only if p < z.
Bridge lemma 2: sieveProduct · selbergTerms(prodPrimes) = ν(prodPrimes).
By Mathlib's selbergTerms_apply:
selbergTerms d = ν(d) · Π_{p|d} (1 - ν(p))⁻¹
For d = prodPrimes: selbergTerms prodPrimes = ν(prodPrimes) · Π_{p|prodPrimes} (1 - ν(p))⁻¹ = ν(prodPrimes) / sieveProduct
Hence sieveProduct · selbergTerms(prodPrimes) = ν(prodPrimes).
Bridge corollary: sieveProduct = ν(prodPrimes) / selbergTerms(prodPrimes).
Distribution identity: for d ≤ D, the counting specialization reads |{a ∈ A : d | a}| = ν(d) · X + R_d.
This is Mathlib's BoundingSieve.multSum_eq_main_err:
multSum d = nu d * totalMass + rem d
Here rem d is the remainder R_d. In applications, the level of distribution D
specifies the range of d on which |rem d| is negligible; this identity alone
does not bound the remainder.
5. Jurkat-Richert-shaped interfaces and Mathlib's sieve upper bound #
Pointwise interface motivated by the Jurkat-Richert upper bound:
S(A, z) ≤ X · V(z) · (F(s) + O(η)) + Σ_{d ≤ D} |R_d|
Relation to Mathlib's siftedSum_le_mainSum_errSum_of_upperMoebius:
Mathlib proves siftedSum ≤ totalMass · mainSum(μ⁺) + errSum(μ⁺).
The uniform Jurkat-Richert analysis additionally controls
mainSum(μ⁺) by V(z) · F(s), and errSum by Σ |R_d|.
This is part of the theory behind upper sieve estimates for Ω in Chen's theorem.
This interface only asks for an uncontrolled additive remainder for a single
SP, so the absolute difference of the two sides proves it directly.
It is not the uniform Jurkat-Richert estimate: that would additionally require
an explicit relation between C_error and bounds on SP.rem, as well as
the classical logarithmic sieve ratio rather than the quotient used here.
Pointwise interface motivated by the Jurkat-Richert lower bound:
S(A, z) ≥ X · V(z) · (f(s) - O(η)) - Σ_{d ≤ D} |R_d|
The classical estimate underlies the lower bound on W(N) in Chen's theorem: W(N) ≥ 2.6408 𝔖(N) N/log²N
As above, these quantifiers express only the existence of an additive
remainder for each individual SP; they do not establish a uniform
Jurkat-Richert lower bound.
6. Application to Chen's theorem #
6.5 Scope of Chen's key inequality #
The definitions of W(N) and Ω(N), and their conditional key inequality, are
in SwitchingPrinciple.lean (chenW, chenOmega, chen_key_inequality).
The inequality requires explicit uniform analytic bounds; the pointwise
remainder interfaces here do not supply them. In particular, replacing both
counts by zero would make the required assertion 0 - 0/2 > 0 false.
The historical counting bridge for the current definitions also has the
limitation recorded below.