Mertens products and the corrected main term #
The exact Möbius lower sieve, Selberg divisor products, and truncated singular series yield uniform lower bounds and the asymptotic order of the main term.
All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.
Fundamental-lemma-level lower bound for the corrected sieve #
Key observation for the corrected-candidate lower bound: the ordinary Möbius function is a lower Möbius sequence, with equality.
∑_{d | n} μ(d) = [n = 1] (Möbius inversion, mathlib
ArithmeticFunction.coe_zeta_mul_coe_moebius + coe_zeta_smul_apply),
Thus μ : ℕ → ℝ satisfies IsLowerMoebius.
|μ(d)| ≤ 1, in the real-valued version.
Corrected sieve product: V(N) = ∏_{p | corrected sifting product} (1 - ν(p)),
where ν(p) = 1/(p-1). This is the same product as
sieveProductPrimeFactors in AnalyticNumberTheory.
Equations
Instances For
The Selberg main term for the ordinary Möbius function equals the corrected sieve product, exactly.
∑_{d | P} μ(d)·ν(d) = ∏_{p | P} (1 - ν(p)), the "one-minus" factorization for multiplicative functions
(mathlib prodPrimeFactors_one_sub_of_squarefree). This is the exact form of the JR main term
for corrected candidates: the main term is V(N), without sieve-function asymptotics.
The Möbius error sum is bounded by the unit-coefficient error sum: |μ(d)| ≤ 1 ⇒ errSum(μ) ≤ errSum(1).
Fundamental-lemma-level lower bound for corrected candidates.
card(correctedChenCandidates N) ≥ X·V(N) − errSum(1)
This holds unconditionally for all N, with total mass X = N/log N, corrected sieve product V(N),
and explicit divisor error sum errSum(1) = Σ_{d | P} |rem d|.
Classical counterpart: the fundamental-lemma/linear-sieve lower bound S(A,z) ≥ X·V(z) - Σ_{d ≤ D} |R_d|.
The proof uses only the ordinary Möbius function, which is itself an exact lower Möbius sequence,
so the main term is exactly X·V(N) and no asymptotic for f(s) is needed. This distinguishes
the corrected candidates, which require only that N-p have no prime factor below z,
from the historical W candidates, which impose an additional medium-prime condition. The remaining analytic inputs are:
(1) a uniform Mertens-type lower bound for V(N), giving a main term ≫ N/log²N;
(2) weighted Pan control of errSum(1);
(3) a uniform upper bound for correctedChenOmega.
The corrected Selberg divisor sum splits into the Mertens-type prime product over the sieved primes and the reciprocal of their singular-series local-factor product. This is the finite seam at which the exact Mertens product formula and the singular series enter the main term.
Main-term asymptotics: Mertens products and the singular series #
Main-term identity linking Mertens products to the singular series: the corrected Selberg divisor sum
times the truncated singular series at z - 1 equals the reciprocal of the
exact Mertens primeProduct (z - 1).
This is the exact seam at which the main term connects the Mertens product
formula to the singular series: it restores the excluded p = 2 and p | N
local factors (back into singularSeriesTruncated) and reduces the sieved
Selberg product to the full Mertens-type prime product ∏_{p<z} p/(p-1).
Main-term lower bounds and the singular-series identity #
Positivity of the Mertens prime product: ∏_{p ≤ x}(1 - 1/p) > 0.
selbergSum = 1 / V(N): invert the "one-minus" factorization of the Selberg divisor sum.
Main-term identity through the singular series: the corrected sieve product equals the truncated singular series times the exact Mertens product:
V(N) = 𝔖_trunc(N, z-1) · primeProduct(z-1)
This is the exact identity turning X·V(N) into a main term of the form X·𝔖·primeProduct(z-1):
correctedChenSelbergSum_mul_singularSeriesTruncated
invert selbergSum·𝔖 = primeProduct⁻¹ and selbergSum = V⁻¹.
Uniform main-term lower bound: there exist c > 0 and a threshold N₀ such that
X·V(N) ≥ c·N/log²N for all even N ≥ N₀.
The quantifiers c, N₀ precede ∀ N: the constants must not depend on N.
correctedChenMainTerm_lower_of_estimates derives this from three standard analytic inputs:
(1) a uniform lower bound for 𝔖_trunc; (2) a Mertens lower bound for primeProduct;
(3) the parameter estimate log(z-1) ≤ C·log N.
Equations
- MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenMainTermLower = ∃ (c : ℝ), 0 < c ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → c * ↑N / Real.log ↑N ^ 2 ≤ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBoundingSieve N).totalMass * MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSieveProduct N
Instances For
Pointwise assembly of the main-term lower bound: given (1) c𝔖 ≤ 𝔖_trunc,
(2) the Mertens lower bound cpp/log(z-1) ≤ primeProduct(z-1), and (3) the parameter estimate
log(z-1) ≤ Clog·log N, we obtain
c𝔖·cpp/Clog · N/log²N ≤ X·V(N).
The proof uses only V = 𝔖_trunc·primeProduct(z-1) and positivity/reciprocal arithmetic.
Package three uniform analytic inputs into CorrectedChenMainTermLower:
(1) a uniform lower bound for 𝔖_trunc; (2) a uniform Mertens lower bound for primeProduct;
(3) the parameter estimate log(z-1) ≤ Clog·log N; also assume (4) the parameter condition
(2 ≤ N、2 ≤ z-1、M₀ ≤ z-1).
Parameter estimates linking Mertens products and the singular series #
Parameter estimate 1: the corrected sieve level satisfies z - 1 ≤ N in ℝ.
Parameter estimate 2: for N ≥ 3^10 = 59049, the corrected sieve level satisfies 2 ≤ z - 1.
Parameter estimate 3: log(z - 1) ≤ log N, the estimate with Clog = 1.
The uniform main-term lower bound follows from (1) the uniform singular-series lower bound h𝔖
(at the scale of C₂) and (2) the proved Mertens product estimate primeProduct_asymptotic_order,
together with the proved parameter estimates. The only analytic input to this implication is h𝔖.
Uniform lower bound for the truncated singular series.
For any N and z ≥ 2, 1/2 ≤ 𝔖_trunc(N, z). The classical proof, at the scale
of the twin-prime constant C₂ ≈ 0.66, is:
𝔖_trunc(N,z) ≥ ∏{2<p≤z}(1 − 1/(p−1)²) ≥ 1 − Σ{p>2} 1/(p−1)² ≥ 1 − (1/4)·Σ_{k≥1} 1/k² ≥ 1/2,
The second line uses ∏(1-x_i) ≥ 1-Σx_i; the third uses that p-1 lies in the even numbers
for primes p > 2; the last uses the telescoping bound Σ_{k≥1}1/k² ≤ 2. The proof is purely
finite combinatorics and real arithmetic. This precisely stated proposition, through
CorrectedChenMainTermLower_of_singularSeries_lower, directly yields the main-term lower bound.
Equations
- MathlibNt.SieveTheory.SwitchingPrinciple.SingularSeriesTruncatedLowerBound = ∀ (N z : ℕ), 2 ≤ z → 1 / 2 ≤ AnalyticNumberTheory.Sieve.singularSeriesTruncated N z
Instances For
The uniform truncated singular-series lower bound with c𝔖 = 1/2 implies CorrectedChenMainTermLower.
Uniform lower bound for the truncated singular series #
The following are general analytic facts, independent of the particular sieve problem.
They concern the finite singular-series products used in
AnalyticNumberTheory/Sieve/SingularSeries.lean.
Σ_{p prime, 2 < p ≤ z} 1/(p-1)² ≤ 1/2.
Primes > 2 are odd, so p-1 = 2k is even. The injection p ↦ (p-1)/2 reduces the sum to
Σ_k 1/(2k)² = (1/4)Σ_k 1/k²; then use the telescoping estimate
Σ_{k≥1} 1/k² ≤ 1 + Σ_{k≥2} 1/((k−1)k) ≤ 2.
Uniform truncated singular-series lower bound: for all N and z ≥ 2, 1/2 ≤ 𝔖_trunc(N, z).
Classical argument at the scale of the twin-prime constant C₂: separate the local factors into p=2, p|N, and p∤N.
Then 𝔖_trunc ≥ ∏_{2<p≤z}(1 - 1/(p-1)²), and combine
∏(1-x_i) ≥ 1-Σx_i with Σ_{p>2}1/(p-1)² ≤ 1/2.
The uniform singular-series lower bound gives the uniform main-term lower bound without further analytic inputs.
Asymptotic order of the main term: the corrected Selberg divisor sum for the corrected sieve
is Θ(log (z-1) / 𝔖(N, z-1)).
This applies the exact Mertens product formula
(primeProduct_asymptotic_order) to the seam
SelbergSum · 𝔖 = 1 / primeProduct (z-1).