AnalyticNumberTheory.Sieve.SelbergUpperBound #
Generic Selberg upper-bound sieve #
The Selberg sieve is a central tool for the upper bound on Ω in
Chen's theorem. An upper Moebius sequence from Λ² weights separates
the sifted count into a main term and a remainder. The classical
shape (Halberstam--Richert 1974 Ch. 3; Nathanson GTM 164 Ch. 10;
Liu 2022 §III) is
S(A,P,z) ≤ X/G(z) + Σ |R_d|, where
G(z) = Σ_{d|P} g(d) and
g(d) = ν(d)·∏_{p|d}(1−ν(p))⁻¹.
For the full divisor sum used here, optimal Λ² weights attain
mainSum = 1/G(z).
This module supplies:
SelbergWeights, a generic bounded, supported weight structure, and its trivial existence theoremselberg_sieve_weights_exist.- Bridges to mathlib's
BoundingSieve.lambdaSquared:selberg_lambda_is_upper_moebius, the basic upper boundomega_upper_bound_via_mathlib, diagonalizationmainSum_diag_via_mathlib, and the Cauchy--Schwarz lower boundmainSum_cauchy_schwarz_lower_bound. - Explicit optimal full-divisor weights
optimalSelbergWeight, withmainSum(Λ²w*) = (Σg)⁻¹(optimalSelbergMainSum_eq), giving the finite theoremselberg_upper_bound_optimalwithout additional analytic input. UniformSelbergUpperBoundfor a family ofBoundingSievestructures, withN₀before∀ N, proved directly from the optimal-weight theorem. The numerical Chen bound3.9404·𝔖(N)·N/log²Nadditionally requires Mertens/singular-series main-term estimates and a weighted Pan remainder input (WeightedPan); the finite theorem does not supply them.
References:
- Selberg, A. (1947), Norske Vid. Selsk. Forh. Trondheim 19, 75-79
- Halberstam & Richert, "Sieve Methods" (1974), Ch. 3
- Nathanson, "Additive Number Theory: The Classical Bases" (1996), Ch. 10
- Liu, Z. (2022), arXiv:2203.07871, §III
- Mathlib
SelbergSieve.lean: BoundingSieve, Λ² sieve, selbergTerms
1. Selberg weight structure #
Selberg weights for a sieve product Q and level z:
λ₁ = 1, λ_d = 0 if d > z or d ∤ Q, and |λ_d| ≤ 1.
This generalizes the Chen-specific SelbergWeights (N ε),
where Q = selbergQ N ε is the product of primes at most z
not dividing N, and z = N^(1/4-ε/2).
The weight function
λ_d.λ₁ = 1
λ_d = 0ifd > zord ∤ Q.|λ_d| ≤ 1
Instances For
Trivial Selberg weights: λ₁ = 1 and all other weights zero
give valid SelbergWeights, with
Σ_{d₁,d₂} λ_{d₁}λ_{d₂}/φ([d₁,d₂]) = 1,
since only d₁ = d₂ = 1 contributes.
This is the trivial comparison choice for the optimal weights
in Chen's Lemma 3.
2. Bridges to mathlib #
Construct mathlib's Λ² weights from SelbergWeights:
lambdaSquared weights d = Σ_{d₁|d} Σ_{d₂|d} [d=lcm(d₁,d₂)]·weights(d₁)·weights(d₂).
Instances For
The lambdaSquared sequence from Selberg weights
is an upper Moebius sequence.
Basic Selberg upper bound (mathlib): any sequence w
with w 1 = 1 gives
siftedSum ≤ totalMass·mainSum(Λ²w) + errSum(Λ²w).
Choosing weights minimizing mainSum gives the optimal finite
upper bound; the remainder still needs separate control.
Main-term diagonalization (mathlib): mainSum(Λ²w) is a
diagonal quadratic form with coefficients (selbergTerms l)⁻¹.
Optimality lower bound (Cauchy--Schwarz/Titu):
for w 1 = 1,
mainSum(Λ²w) ≥ (Σ_{l|P} selbergTerms l)⁻¹.
Optimal Selberg weights attain equality
(optimalSelbergMainSum_eq).
3. Optimal Selberg weights #
Optimal Selberg main term: (Σ_{l|P} selbergTerms l)⁻¹.
Equations
Instances For
Optimal diagonal values x*_l = g(l)·μ(l)·(Σg)⁻¹,
minimizing Σ_l g(l)⁻¹·x_l² subject to w(1)=1.
Equations
Instances For
Optimal Selberg Λ² weights: apply upper-interval Moebius
inversion to optimalSelbergX on the divisor lattice of prodPrimes,
then divide by the density:
w*(d) = ν(d)⁻¹·Σ_{e : d|e|P} μ(e/d)·x*_e.
optimalSelbergMainSum_eq proves
mainSum(Λ²w*) = (Σg)⁻¹, attaining the lower bound
mainSum_cauchy_schwarz_lower_bound.
Equations
- AnalyticNumberTheory.Sieve.optimalSelbergWeight S d = if _hd : d ∣ S.prodPrimes then (∑ e ∈ S.prodPrimes.divisors, if d ∣ e then ↑(ArithmeticFunction.moebius (e / d)) * AnalyticNumberTheory.Sieve.optimalSelbergX S e else 0) / S.nu d else 0
Instances For
Standard Moebius sum: Σ_{d|n} μ(d) = [n=1].
Normalization of the optimal weight: w*(1) = 1.
Diagonal-value identification:
Σ_{d : l|d|P} ν(d)·w*(d) = x*_l.
This is the upper-interval Moebius-inversion identity for
w* = ν⁻¹·y*, where
y*(d) = Σ_{e : d|e|P} μ(e/d)·x*_e.
Optimal main-term identity:
mainSum(Λ²w*) = (Σ_{l|P} selbergTerms l)⁻¹,
the equality case of mainSum_cauchy_schwarz_lower_bound.
Finite Selberg upper bound: optimal Λ² weights minimize
the main term and give
siftedSum ≤ totalMass·(Σ_{l|P} selbergTerms l)⁻¹ + errSum(Λ²w*).
This is the exact finite form of S ≤ X/G(z) + R
(Halberstam--Richert 1974 Ch. 3).
In the Chen application, estimates of the indicated
(Σg)⁻¹ ≈ 8𝔖(N)/log N shape and errSum ≪ N/log^A N
require separate Mertens/singular-series and weighted Pan inputs.
Sieve-product form of the Selberg main term:
for any BoundingSieve,
(Σ_{d|P} selbergTerms d)⁻¹ = ∏_{p|P} (1−ν(p)).
Invert selbergSum_eq_prod_inv, namely
Σg = ∏(1−ν(p))⁻¹.
For a SieveProblem, the product is sieveProduct
(selbergMainTerm_eq_sieveProduct).
For a classical SieveProblem,
(Σ_{d|P} selbergTerms d)⁻¹ = sieveProduct.
Sieve-product upper bound: for a SieveProblem,
optimal Λ² weights give
siftedSum ≤ totalMass·V(z) + errSum(Λ²w*),
where V(z) = sieveProduct.
The identity (Σg)⁻¹ = V(z) is the main-term form used in
the Chen upper bound for Ω; estimates for V(z) come from
Mertens and singular-series analysis.
3.7 Moebius weights attain the full-divisor optimum #
Moebius weights satisfy the optimal diagonal equations:
Σ_{d : l|d|P} ν(d)·μ(d) = x*_l = g(l)·μ(l)·T.
Main term for Moebius weights:
mainSum(Λ²μ) = (Σ_{d|P} selbergTerms d)⁻¹.
Moebius-weight Selberg upper bound: with w=μ,
siftedSum ≤ totalMass·(Σ selbergTerms)⁻¹ + errSum(Λ²μ);
the coefficients satisfy |μ| ≤ 1.
Selberg upper bound with the remainder grouped by modulus: for the optimal full-divisor Moebius Λ² weights, `siftedSum ≤ totalMass·(Σ_{d|P} selbergTerms d)⁻¹
- Σ_{d|P} 3^{ω(d)}·|rem d|
. This is the exact finiteS ≤ X/G(z) + Σ 3^{ω(d)}|Δ(d)|` form. The Chen application controls the main term using Mertens/singular-series estimates and the remainder using the weighted Pan input.
4. Uniform finite Selberg upper bound #
Uniform Selberg upper-bound proposition.
The classical shape (Halberstam--Richert Ch. 3, Chen application)
for sufficiently large even N is
S(A,z) ≤ X/G(z) + Σ |R_d|, with G(z)=Σ_{d|P}g(d).
The finite formulation asks for N₀ such that for every even
N ≥ N₀ there is a sequence w, w 1 = 1, satisfying
siftedSum ≤ totalMass·(Σ_{d|P}g(d))⁻¹ + errSum(Λ²w).
The threshold precedes ∀ N. selberg_upper_bound_optimal
proves this for every BoundingSieve family without additional
analytic assumptions (uniformSelbergUpperBound).
The numerical Chen bound 3.9404·𝔖(N)·N/log²N still requires
Mertens/singular-series main-term control of the indicated
(Σg)⁻¹ ≈ 8𝔖(N)/log N shape and a weighted Pan error estimate
errSum = O(N/log^A N); see WeightedPan.
Equations
- AnalyticNumberTheory.Sieve.UniformSelbergUpperBound SP = ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (w : ℕ → ℝ), w 1 = 1 ∧ BoundingSieve.siftedSum ≤ (SP N).totalMass * (∑ l ∈ (SP N).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ + BoundingSieve.errSum (BoundingSieve.lambdaSquared w)
Instances For
Optimal Selberg weights give the uniform finite upper bound for every sieve family.
5. Numerical coefficient in Chen's theorem #
8 × 0.49254 = 3.94032: the arithmetic behind the main-term
coefficient in the Chen upper bound for Ω, combining the
numerical integral 0.49254 in Chen 1973, equation (28),
with the Selberg diagonalization coefficient 8.