MathlibNt.SieveTheory.SelbergUpperBound

Selberg sieve and the target bound Ω ≤ 3.9404 𝔖(N) N/log²N

The Selberg sieve is a central tool for the upper bound on Ω in Chen's theorem. Selberg upper-bound weights λ_d lead to a main term M₁ and a remainder R.

Classical proof outline (Liu 2022, §III):

1. Selberg weights (Lemma 3): construct λ_d with

   • λ₁ = 1 and λ_d = 0 for d > z or d ∤ Q;
   • |λ_d| ≤ 1;
   • Σ_{d₁,d₂} λ_{d₁}λ_{d₂}/φ([d₁,d₂]) = [8 + O(ε)] 𝔖(N)/log N.

2. Numerical integration (Lemma 4): Σ_a f(a)/(a log(N/a)) ≤ 0.49254/log N.

3. Main term: for suitably controlled ε, M₁ ≤ [8 + O(ε)] · 0.49254 · 𝔖(N) N/log²N ≤ 3.94033 𝔖(N) N/log²N.

4. Remainder: R ≪ N/log^A N, using Pan's mean-value theorem.

5. Combination: Ω ≤ M₁ + |R| ≤ 3.9404 𝔖(N) N/log²N.

This module connects the development to Mathlib.NumberTheory.SelbergSieve and proves finite algebraic and divisor-sum results. The interfaces for the numerical main and error terms below allow constants depending on a fixed N; they do not establish the uniform optimized bounds in this classical outline.

References:

• Selberg, A. (1947), Norske Vid. Selsk. Forh. Trondheim 19, 75-79
• Liu, Z. (2022), arXiv:2203.07871, Lemma 3-4, §III
• Halberstam & Richert, "Sieve Methods" (1974), Ch. 3
• Mathlib SelbergSieve.lean: BoundingSieve, SelbergSieve, Λ² sieve

1. Selberg sieve weights (Lemma 3)

noncomputable def MathlibNt.SieveTheory.SelbergUpperBound.selbergQ (N : ℕ) (ε : ℝ) : ℕ

Q is the product of primes ≤ z = N^(1/4 - ε/2) that do not divide N.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.selbergQ N ε = {p ∈ Finset.range (⌊↑N ^ (1 / 4 - ε / 2)⌋₊ + 1) | Nat.Prime p ∧ ¬p ∣ N}.prod id

structure MathlibNt.SieveTheory.SelbergUpperBound.SelbergWeights (N : ℕ) (ε : ℝ) : Type

Selberg weight conditions (Lemma 3, Liu 2022). The structure records:

1. λ₁ = 1
2. λ_d = 0 when d > z or d ∤ Q
3. |λ_d| ≤ 1

The classical optimized weights additionally satisfy Σ_{d₁,d₂} λ_{d₁}λ_{d₂}/φ([d₁,d₂]) = [8 + O(ε)] 𝔖(N)/log N; this quadratic-form estimate is not a field of the structure.

• lambda : ℕ → ℝ

  The weight function λ_d.

• lambda_one : self.lambda 1 = 1

  λ₁ = 1

• lambda_support (d : ℕ) : d > ⌊↑N ^ (1 / 4 - ε / 2)⌋₊ ∨ ¬d ∣ selbergQ N ε → self.lambda d = 0

  λ_d = 0 when d > z or d ∤ Q.

• lambda_bounded (d : ℕ) : |self.lambda d| ≤ 1

  |λ_d| ≤ 1

theorem MathlibNt.SieveTheory.SelbergUpperBound.selberg_sieve_weights_exist (N : ℕ) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 1 / 2) (hN : 2 ≤ N) : ∃ (SW : SelbergWeights N ε) (C : ℝ), |∑ d₁ ∈ (selbergQ N ε).divisors, (∑ d₂ ∈ (selbergQ N ε).divisors, SW.lambda d₁ * SW.lambda d₂ / ↑(d₁.lcm d₂).totient - 8 * 1 / Real.log ↑N)| ≤ C * ε / Real.log ↑N

Pointwise interface for Selberg weights, motivated by Lemma 3:

Σ_{d₁,d₂} λ_{d₁}λ_{d₂}/φ([d₁,d₂]) = [8 + O(ε)] 𝔖(N)/log N

The uniform version is a key ingredient in estimating the main term M₁ for Ω.

The constant C here has no uniformity, positivity, or compatibility requirements with other sieve data. Explicit δ₁ weights therefore suffice, with C absorbing the difference. This is not the optimized Selberg-weight estimate of Liu/Wang, which needs a controlled error suitable for comparing main terms.

2. Numerical integration (Lemma 4)

theorem MathlibNt.SieveTheory.SelbergUpperBound.lemma4_numerical_bound (N : ℕ) (hN : 2 ≤ N) : ∃ (C : ℝ), ∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0) / (↑a * Real.log (↑N - ↑a)) ≤ 0.49254 / Real.log ↑N + C / Real.log ↑N ^ 2

Pointwise interface motivated by Lemma 4 (Liu 2022). For the indicator f(a) of a = p₁p₂ satisfying the range conditions, the classical target is

Σ_a f(a)/(a log(N/a)) ≤ 0.49254 / log N

Partial summation leads to the double-integral expression = (1/log N) ∫{1/10}^{1/3} dα/α ∫{1/3}^{(1-α)/2} dβ/(β(1-α-β)) < 0.49254 / log N

Here C may depend on the individual N, with no uniformity requirement. This interface gives only the algebraic existence of a pointwise remainder, not a formalization of the uniform analytic integral estimate above.

theorem MathlibNt.SieveTheory.SelbergUpperBound.integral_margin : 0.49253 < 0.49254

Numerical margin used by the Lemma 4 interface: 0.49253 < 0.49254.

This theorem does not formalize the motivating double integral. The integral estimate in the literature requires a separate formalization using MeasureTheory / IntervalIntegral.

3. Estimating the main term M₁

noncomputable def MathlibNt.SieveTheory.SelbergUpperBound.logarithmicIntegral_approx_term (x : ℝ) : ℝ

The logarithmic-integral approximation term used here.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.logarithmicIntegral_approx_term x = x / Real.log x

theorem MathlibNt.SieveTheory.SelbergUpperBound.logarithmicIntegral_approx (x : ℝ) (hx : 2 ≤ x) : ∃ (C : ℝ), |logarithmicIntegral_approx_term x - x / Real.log x| ≤ C * x / Real.log x ^ 2

Interface with the shape of li(x) = x/log x + O(x/log²x).

Since logarithmicIntegral_approx_term x = x / log x by definition, the difference is zero and C = 0 suffices. This is not an estimate of the analytic logarithmic integral.

theorem MathlibNt.SieveTheory.SelbergUpperBound.main_term_bound (N : ℕ) (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 1 / 2) (hN : 2 ≤ N) (SW : SelbergWeights N ε) : ∃ (C : ℝ), ∑ d₁ ∈ (selbergQ N ε).divisors, ∑ d₂ ∈ (selbergQ N ε).divisors, SW.lambda d₁ * SW.lambda d₂ / ↑(d₁.lcm d₂).totient * ∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0) * logarithmicIntegral_approx_term (↑N / ↑a) ≤ 3.94033 * 1 * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ 10

Main term M₁, with a pointwise remainder: M₁ = Σ_{d₁,d₂} λ_{d₁}λ_{d₂}/φ([d₁,d₂]) · Σ_a f(a) · li(N/a)

The classical Lemmas 3 and 4, with controlled errors, would give M₁ ≤ [8 + O(ε)] 𝔖(N)/log N · 0.49254 N/log N ≤ 3.94033 𝔖(N) N/log²N.

SelbergWeights encodes normalization, support, and |lambda d| ≤ 1, but not optimality or the quadratic-form estimate above. These structural hypotheses do not imply a remainder-free 3.94033 bound for arbitrary SW. This theorem retains the existence of an additive remainder for fixed N; a uniform controlled C requires the actual Selberg quadratic-form estimate.

theorem MathlibNt.SieveTheory.SelbergUpperBound.coefficient_product : 8 * 0.49254 = 3.94032

8 × 0.49254 = 3.94032

4. Estimating the remainder R

def MathlibNt.SieveTheory.SelbergUpperBound.primesInAP (x q l : ℕ) : ℕ

Local definition: π(x; q, l) = |{p ≤ x : p prime, p ≡ l (mod q)}|.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.primesInAP x q l = {p ∈ Finset.range (x + 1) | Nat.Prime p ∧ p ≡ l [MOD q]}.card

theorem MathlibNt.SieveTheory.SelbergUpperBound.error_term_bound (N : ℕ) (ε A : ℝ) (_hA : 0 < A) (_hε : 0 < ε) (hN : 2 ≤ N) (_SW : SelbergWeights N ε) : ∃ (C : ℝ), |∑ d ∈ (selbergQ N ε).divisors with ↑d ≤ ↑N ^ (1 / 2 - ε), 3 ^ d.primeFactors.card * ∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0) * (↑(primesInAP N d (N % d)) - logarithmicIntegral_approx_term (↑N / ↑a) / ↑d.totient)| ≤ C * ↑N / Real.log ↑N ^ A

Remainder R: the Selberg sieve expansion leads to

|R| ≤ Σ_{d|Q, d ≤ N^(1/2-ε)} 3^ω(d) |Σ_a f(a) Δ(N; a, d, N)|

The factor 3^ω(d) counts pairs (d₁,d₂) with [d₁,d₂] = d. The intended uniform estimate R ≪ N/log^A N uses Pan's mean-value theorem.

The quantifiers here allow C to depend on the individual N and the entire error sum. This establishes only a pointwise algebraic interface, not the uniform constant required by Pan's mean-value theorem.

theorem MathlibNt.SieveTheory.SelbergUpperBound.lcm_pair_count (d : ℕ) (_hd : d ≠ 0) (hsq : Squarefree d) : {x ∈ d.divisors ×ˢ d.divisors | match x with | (d₁, d₂) => d₁.lcm d₂ = d}.card = 3 ^ d.primeFactors.card

Origin of 3^ω(d): the number of pairs (d₁, d₂) with [d₁, d₂] = d is 3^ω(d).

This holds only for squarefree d. At each prime factor p of d, where v_p(d) = 1, the exponents in (d₁, d₂) have three possibilities: (0, 1), (1, 0), (1, 1) and hence the total is 3^ω(d).

For nonsquarefree d, the formula is ∏_p (2v_p(d) + 1), not 3^ω(d). For example, d = 4 gives 5 pairs, whereas 3^1 = 3. In Chen's sieve, d | Q and Q is a product of distinct primes, so d is squarefree.

A strong-induction proof has the following structure:

• Base: d = 1 gives count = 1 = 3^0.
• Step: d = p · d', with p prime and gcd(p, d') = 1.
  • divisors(d) = divisors(d') ⊔ (p · divisors(d')), by coprimality.
  • Three cases each give f(d') pairs: A) p|d₁, p|d₂: lcm(pa, pb) = p·lcm(a,b) = p·d' ⟺ lcm(a,b) = d' B) p|d₁, p∤d₂: lcm(pa, b) = p·lcm(a,b), since gcd(p,b)=1; as above C) p∤d₁, p|d₂: symmetric to B D) p∤d₁, p∤d₂: impossible, since then p ∤ lcm(d₁,d₂) = d
  • Thus f(d) = 3·f(d') = 3·3^ω(d') = 3^(ω(d')+1) = 3^ω(d). The proof below applies Mathlib's existing counting theorem.

5. Combined upper-bound interfaces for Ω

theorem MathlibNt.SieveTheory.SelbergUpperBound.chenOmega_complete_bound (N : ℕ) (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 1 / 2) (_hN : Even N) (hN_large : 2 ≤ N) : ∃ (C : ℝ), (∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0) * ∑ p₃ ∈ Finset.range (N + 1), if Nat.Prime p₃ ∧ a * p₃ ≤ N ∧ Nat.Prime (N - a * p₃) then 1 else 0) ≤ 3.9404 * 1 * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ 10

Combined pointwise interface for Ω, motivated by the target Ω ≤ M₁ + |R| ≤ 3.9404 𝔖(N) N/log²N.

Classical proof outline:

1. Ω ≤ Σ_a f(a) Σ_{ap ≤ N, (N-ap, Q)=1} 1 + N^(2/3) z, by prime factorization.
2. Bound this by Σ_a f(a) Σ_{ap ≤ N} (Σ_d λ_d)² + N^(11/12), using the Selberg upper sieve.
3. Exchange the sums to obtain the main term M₁ and remainder R.
4. Bound M₁ ≤ 3.94033 𝔖(N) N/log²N, using Lemmas 3 and 4.
5. Bound |R| ≪ N/log^A N, using Pan's mean-value theorem.
6. Combine to get Ω ≤ 3.9404 𝔖(N) N/log²N.

The conclusion below allows C to depend on the individual N. It therefore establishes an interface with a pointwise additive remainder, not the uniform remainder-free conclusion in this outline.

theorem MathlibNt.SieveTheory.SelbergUpperBound.chenOmega_simple_bound (N : ℕ) (hN : Even N) (hN_large : 1000 ≤ N) : ∃ (C : ℝ), (∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0) * ∑ p₃ ∈ Finset.range (N + 1), if Nat.Prime p₃ ∧ a * p₃ ≤ N ∧ Nat.Prime (N - a * p₃) then 1 else 0) ≤ 3.9404 * 1 * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ 10

Pointwise form without the ε parameter.

Take ε = 1/4 in chenOmega_complete_bound. Since its C may depend on the fixed N, the additive remainder must be retained. A uniform remainder-free 3.9404 bound requires optimized Selberg weights and a uniform version of Pan's mean-value theorem.

6. Correspondence with Mathlib's Selberg sieve

def MathlibNt.SieveTheory.SelbergUpperBound.selbergLambdaSquared {N : ℕ} {ε : ℝ} (SW : SelbergWeights N ε) : ℕ → ℝ

Construct Mathlib's lambdaSquared weights from SelbergWeights.

Mathlib: lambdaSquared weights d = Σ_{d₁|d} Σ_{d₂|d} if d = lcm(d₁,d₂) then weights(d₁)·weights(d₂) else 0

Here SW.lambda supplies Mathlib's weights parameter, and lambdaSquared gives the Selberg coefficients λ_d = Σ_{[d₁,d₂]=d} λ_{d₁}·λ_{d₂}.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.selbergLambdaSquared SW = BoundingSieve.lambdaSquared SW.lambda

theorem MathlibNt.SieveTheory.SelbergUpperBound.selberg_lambda_is_upper_moebius {N : ℕ} {ε : ℝ} (SW : SelbergWeights N ε) : BoundingSieve.IsUpperMoebius (selbergLambdaSquared SW)

Bridge theorem 1: lambdaSquared constructed from the Selberg weights is upper Möbius.

Apply Mathlib's upperMoebius_lambdaSquared: if weights 1 = 1, then lambdaSquared weights satisfies IsUpperMoebius.

The field SelbergWeights.lambda_one supplies exactly lambda 1 = 1.

theorem MathlibNt.SieveTheory.SelbergUpperBound.omega_upper_bound_via_mathlib (S : BoundingSieve) (w : ℕ → ℝ) (hw : w 1 = 1) : BoundingSieve.siftedSum ≤ S.totalMass * BoundingSieve.mainSum (BoundingSieve.lambdaSquared w) + BoundingSieve.errSum (BoundingSieve.lambdaSquared w)

Bridge theorem 2: Mathlib's siftedSum_le_mainSum_errSum_of_upperMoebius gives the generic upper sieve bound.

For a BoundingSieve encoding the sieve problem, any weights w with w 1 = 1 give upper Möbius coefficients lambdaSquared w, and hence siftedSum ≤ totalMass · mainSum(lambdaSquared w) + errSum(lambdaSquared w)

The target Chen bound Ω ≤ 3.9404 𝔖(N) N/log²N additionally requires an optimized estimate of mainSum(lambdaSquared w) on the scale 8 𝔖(N)/log N and errSum(lambdaSquared w) ≪ N/log^A N. Selberg diagonalization and Pan's mean-value theorem motivate these two inputs; the pointwise interfaces selberg_sieve_weights_exist and error_term_bound do not by themselves supply their uniform versions.

theorem MathlibNt.SieveTheory.SelbergUpperBound.mainSum_diag_via_mathlib (S : BoundingSieve) (w : ℕ → ℝ) : BoundingSieve.mainSum (BoundingSieve.lambdaSquared w) = ∑ l ∈ S.prodPrimes.divisors, (BoundingSieve.selbergTerms l)⁻¹ * (∑ d ∈ S.prodPrimes.divisors, if l ∣ d then S.nu d * w d else 0) ^ 2

Bridge theorem 3: diagonalization of the main term via Mathlib's mainSum_lambdaSquared_eq_sum_mul_sum_sq.

For any weights w, Mathlib proves mainSum(lambdaSquared w) = Σ_{l | P} (selbergTerms l)⁻¹ · (Σ_{l|d|P} ν(d)·w(d))²

This underlies the choice of optimal Selberg weights: minimizing the quadratic form gives mainSum = (Σ_{l|P} selbergTerms l)⁻¹ in the unrestricted divisor setup.

For Chen's theorem, the corresponding level-restricted optimization and analytic estimates are the basis of Lemma 3's mainSum bound at scale 8 𝔖(N)/log N; diagonalization alone does not prove that estimate.

theorem MathlibNt.SieveTheory.SelbergUpperBound.mainSum_cauchy_schwarz_lower_bound (S : BoundingSieve) (w : ℕ → ℝ) (hw : w 1 = 1) : (∑ l ∈ S.prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ ≤ BoundingSieve.mainSum (BoundingSieve.lambdaSquared w)

Bridge theorem 4: the Selberg-sieve Cauchy-Schwarz lower bound.

For the diagonal variables x_l = Σ_{l|d|P} ν(d)·w(d), Möbius inversion and w(1) = 1 give Σ_l μ(l)x_l = 1. Cauchy-Schwarz, with a_l = (selbergTerms l)⁻¹, gives Σ_l a_l x_l² ≥ (Σ_l μ(l)x_l)² / (Σ_l μ(l)²/a_l). All l | P are squarefree, so μ(l)² = 1. Therefore mainSum ≥ 1 / (Σ_l selbergTerms l).

The signed Möbius identity is essential: no positivity assumption on w justifies replacing it by a claim that x_1 ≥ 1.

Equality characterizes the optimal Selberg weights on the relevant divisors, for which mainSum = (Σ_{l|P} selbergTerms l)⁻¹.

The classical Chen calculation seeks the corresponding level-restricted estimate Σ_{l|P} selbergTerms l ≈ log N / (8 𝔖(N)) and hence the optimized mainSum scale 8 𝔖(N) / log N (Lemma 3).

Cauchy-Schwarz gives a lower bound, not an upper bound: mainSum ≥ (Σ selbergTerms)⁻¹ for every normalized w, with equality only for optimal weights. The theorem below proves this finite lower bound.

7. Auxiliary definition: π(x; a, q, l)

def MathlibNt.SieveTheory.SelbergUpperBound.primesInAP_weighted (x a q l : ℕ) : ℕ

π(x; a, q, l) = |{p ≤ x : ap prime, ap ≡ l (mod q)}|.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.primesInAP_weighted x a q l = {p ∈ Finset.range (x + 1) | Nat.Prime (a * p) ∧ a * p ≡ l [MOD q]}.card

noncomputable def MathlibNt.SieveTheory.SelbergUpperBound.weightedDistributionError (x a q l : ℕ) : ℝ

Δ(x; a, q, l) = π(x; a, q, l) - li(x/a)/φ(q)

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.weightedDistributionError x a q l = ↑(MathlibNt.SieveTheory.SelbergUpperBound.primesInAP_weighted x a q l) - MathlibNt.SieveTheory.SelbergUpperBound.logarithmicIntegral_approx_term (↑x / ↑a) / ↑q.totient

6.5a. Ingredients for divisor_sum_bound

noncomputable def MathlibNt.SieveTheory.SelbergUpperBound.divisorWeight (A : ℝ) : ArithmeticFunction ℝ

Weight f(d) = A^{ω(d)}/φ(d), with f(0) = 0.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.divisorWeight A = { toFun := fun (d : ℕ) => A ^ d.primeFactors.card / ↑d.totient, map_zero' := ⋯ }

noncomputable def MathlibNt.SieveTheory.SelbergUpperBound.zetaR : ArithmeticFunction ℝ

The real-valued zeta arithmetic function: 1 on positive integers, 0 at zero.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.zetaR = { toFun := fun (n : ℕ) => if n = 0 then 0 else 1, map_zero' := MathlibNt.SieveTheory.SelbergUpperBound.zetaR._proof_1 }

6.5. Lemma 2 (divisor-sum bound)

theorem MathlibNt.SieveTheory.SelbergUpperBound.divisor_sum_bound (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), ∀ (n : ℕ), 1 ≤ n → ∑ d ∈ n.divisors, A ^ d.primeFactors.card / ↑d.totient ≤ C * Real.log (Real.log (3 * ↑n)) ^ A

Divisor-sum bound strengthening Lemma 2 (Liu 2022). For A > 0 and n ≥ 1, the source statement is Σ_{d|n} μ²(d) A^ω(d)/φ(d) ≪ (log log 3n)^A

The theorem below proves the stronger bound without μ²(d). In particular, if n is a product of distinct primes ≤ y and y ≥ 3, the sum is ≪ (log y)^A.

This gives the estimate Σ 3^ω(d)/φ(d) ≪ (log N)³ used for the remainder R₁.

theorem MathlibNt.SieveTheory.SelbergUpperBound.divisor_sum_bound_mu2 (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), ∀ (n : ℕ), 1 ≤ n → ∑ d ∈ n.divisors, ↑(ArithmeticFunction.moebius d) ^ 2 * (A ^ d.primeFactors.card / ↑d.totient) ≤ C * Real.log (Real.log (3 * ↑n)) ^ A

Source form of Lemma 2 (Liu 2022): Σ_{d|n} μ²(d)·A^{ω(d)}/φ(d) ≪ (log log 3n)^A.

The notation matches Liu 2022, Lemma 2, arXiv:2203.07871:

• ω(d) is the number of distinct prime factors of d (d.primeFactors.card);
• φ(d) is Euler's totient function (Nat.totient d);
• μ²(d) is the square of the Möbius function, the squarefree indicator;
• the upper-bound scale is (log log 3n)^A, for fixed A > 0.

divisor_sum_bound proves the stronger version without μ², summing over all divisors. Since every summand is nonnegative and μ²(d) ∈ {0,1}, that version implies the source statement.

noncomputable def MathlibNt.SieveTheory.SelbergUpperBound.chenDivisorWeight (A : ℝ) : ArithmeticFunction ℝ

Divisor-sum weight f(d) = A^{ω(d)}/φ(d), as an arithmetic function with f(0) = 0.

Equations

• MathlibNt.SieveTheory.SelbergUpperBound.chenDivisorWeight A = { toFun := fun (d : ℕ) => A ^ d.primeFactors.card / ↑d.totient, map_zero' := ⋯ }

theorem MathlibNt.SieveTheory.SelbergUpperBound.divisor_sum_bound_squarefree (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), ∀ (n y : ℕ), 1 ≤ n → Squarefree n → (∀ (p : ℕ), Nat.Prime p → p ∣ n → p ≤ y) → 3 ≤ y → ∑ d ∈ n.divisors, A ^ d.primeFactors.card / ↑d.totient ≤ C * Real.log ↑y ^ A

Special case of Lemma 2: if n is a product of distinct primes ≤ y (that is, Squarefree n and all prime factors are ≤ y), with y ≥ 3, then Σ_{d|n} A^ω(d)/φ(d) ≪ (log y)^A.

Proof:

1. The weight f(d) = A^{ω(d)}/φ(d) is multiplicative, so prodPrimeFactors_one_add_of_squarefree gives Σ_{d|n} f(d) = ∏_{p|n}(1 + f p).
2. At a prime p, f p = A/(p-1), hence ∏{p|n}(1 + A/(p-1)) ≤ exp(A·Σ{p|n} 1/(p-1)).
3. Mertens' theorem (prime_inv_pminus1_bound) gives Σ_{p|n} 1/(p-1) ≤ Σ_{p≤y} 1/(p-1) ≤ log(log y) + C.
4. exp(A·(log(log y) + C)) = e^{AC}·(log y)^A.

The hypotheses explicitly include Squarefree n and 3 ≤ y. Allowing y = 1 would make the right side zero while the left side is at least 1.

theorem MathlibNt.SieveTheory.SelbergUpperBound.divisor_sum_3_omega_bound (N : ℕ) (ε : ℝ) (hε : 0 < ε) (hN : 3 ≤ N) : ∃ (C : ℝ), ∑ d ∈ (selbergQ N ε).divisors, 3 ^ d.primeFactors.card / ↑d.totient ≤ C * Real.log ↑N ^ 3

Application: Σ_{d|Q} 3^ω(d)/φ(d) ≪ (log N)³.

In Chen's sieve, Q is a product of primes ≤ z = N^(1/4-ε/2). Apply Lemma 2 with A = 3 and y = N to obtain the bound.

The hypotheses include 0 < ε and 3 ≤ N. At N = 1, the right side would be zero while the left side is at least 1.

6.6. Liu's correction: the case (a,d)>1 (Section IV)

theorem MathlibNt.SieveTheory.SelbergUpperBound.coprime_condition_implies_bounded_ap (N a d : ℕ) (_hN : 2 ≤ N) (ha : 1 ≤ a) (_hd : 1 ≤ d) (h_not_coprime : 1 < a.gcd d) : primesInAP_weighted N a d (N % d) ≤ 1

(a,d)>1 implies π(N;a,d,N) ≤ 1 for the local counting definition.

When (a,d) > 1 and a ≥ 1, we have a ≥ 2, so ap can be prime only if p = 1. Indeed, a | ap, and primality gives a = 1 or a = a*p. The first case contradicts a ≥ 2, and the second gives p = 1. Thus at most one p satisfies the conditions, and the count is at most 1.

theorem MathlibNt.SieveTheory.SelbergUpperBound.prime_divisor_recip_sum_bounded_real (N : ℕ) (ε : ℝ) (hε : 0 < ε) (hN8 : 8 ≤ N) : ∃ (C₀ : ℝ), 0 ≤ C₀ ∧ ∀ (d : ℕ), d ∣ selbergQ N ε → ∑ p₁ ∈ d.primeFactors with ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3), 1 / ↑p₁ ≤ C₀

Lemma for R₁: for d | Q, Σ_{N^(1/10) < p₁ ≤ N^(1/3), p₁|d} 1/p₁ is bounded uniformly in d.

The sum is at most Σ_{N^(1/10) < p ≤ N^(1/3)} 1/p. Lemma 1, prime_reciprocal_sum_bounded with α = 1/10 and β = 1/3, bounds this by C₀ independently of d.

theorem MathlibNt.SieveTheory.SelbergUpperBound.r1_upper_bound (N : ℕ) (ε : ℝ) (hε : 0 < ε) (hN : ∃ (N₀ : ℕ), N₀ ≤ N) : ∃ (C : ℝ), ∑ d ∈ (selbergQ N ε).divisors, 3 ^ d.primeFactors.card / ↑d.totient * ∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ ∧ 1 < a.gcd d then 1 else 0) * logarithmicIntegral_approx_term (↑N / ↑a) ≤ C * Real.log ↑N ^ 3 * ↑N

R₁ upper-bound interface for the contribution with (a,d)>1:

R₁ ≪ Σ_{d|Q} 3^ω(d)/φ(d) · max Σ_{(a,d)>1} f(a) · li(N/a) ≪ (log N)³ · N

Limitation of an unrestricted divisor estimate (see the known-error discussion in pan-wang-ding-1975.md): the estimate attributed there to Pan et al. (1975) and Liu (2022) is Σ_{p₁|d, p₁>N^(1/10)} 1/p₁ ≪ N^(-1/10), leading to R₁ ≪ N^(9/10)(log N)³. Without a size restriction on d, that reciprocal-sum estimate is false: for d = ∏{N^(1/10)<p≤N^(1/4)} p, the left side tends to the positive constant log(5/2), not to zero. The bound used here instead applies Lemma 1 twice: Σ{p₁|d, p₁∈(N^(1/10),N^(1/3)]} 1/p₁ ≤ C₀, Σ_{p₂∈(N^(1/3),(N/p₁)^(1/2)]} 1/p₂ ≤ C₁. Since li(N/a) ≪ N/a, the inner sum is ≪ N, giving the scale R₁ ≪ (log N)³·N. This suffices for the bound below, not for a uniform N/log^A N error estimate. The theorem's constant is quantified after N.

theorem MathlibNt.SieveTheory.SelbergUpperBound.r1_simplified_bound (N : ℕ) (ε : ℝ) (_hε : 0 < ε) (hN : 2 ≤ N) : ∃ (C : ℝ), ∑ d ∈ (selbergQ N ε).divisors, 3 ^ d.primeFactors.card / ↑d.totient * ∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ ∧ 1 < a.gcd d then 1 else 0) * logarithmicIntegral_approx_term (↑N / ↑a) ≤ C * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Pointwise constant interface at the scale N^(9/10) (log N)².

The constant C may depend on the individual N. A uniform Liu-type bound would require the constant to be quantified before ∀ N.

theorem MathlibNt.SieveTheory.SelbergUpperBound.complete_error_bound_corrected (N : ℕ) (ε A : ℝ) (_hε : 0 < ε) (_hA : 0 < A) (hN : 2 ≤ N) : ∃ (C : ℝ), ∑ d ∈ (selbergQ N ε).divisors, 3 ^ d.primeFactors.card * ∑ a ∈ Finset.range (N + 1), (if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0) * (↑(primesInAP N d (N % d)) - logarithmicIntegral_approx_term (↑N / ↑a) / ↑d.totient) ≤ C * ↑N / Real.log ↑N ^ A

Pointwise interface for the complete error, motivated by Liu's correction and the target R = R₀ + R₁ ≪ N/log^A N.

• R₀ is the part with (a,d)=1, for which Pan's mean-value theorem supplies the intended estimate R₀ ≪ N/log^A N.
• R₁ is the part with (a,d)>1. A uniform estimate R₁ ≪ N^(9/10) (log N)² would imply R₁ ≪ N/log^A N for sufficiently large N.

Liu (2022) addresses the omission of the case (a,d)>1 in Pan et al. (1975).

The quantifier order here still expresses only a pointwise error constant. It does not establish the uniform estimates in this outline, and r1_simplified_bound is also only a pointwise interface.

8. Mathematical scope