AnalyticNumberTheory.Sieve.SingularSeries

Goldbach singular-series factors and finite products

The classical Chen bounds contain the singular-series factor

𝔖(N) = Π_{p|N, p>2} (p-1)/(p-2) · Π_{p>2} (1 - 1/(p-1)²),

whose second product is the twin-prime constant C₂ ≈ 0.66016.... For even N, the local factors used in this module are:

• p = 2: 2;
• p > 2, p | N: p/(p-1);
• p > 2, p ∤ N: p(p-2)/(p-1)².

Thus the local-factor product includes the factor 2, unlike the normalization of 𝔖(N) displayed above. The implemented singularSeries N is the finite product truncated at z=N, not an infinite-product limit. All results below concern these defined finite products.

References:

• Chen, J.R. (1973), Sci. Sinica 16, 157-176
• Liu, Z. (2022), "A Corrected Simplified Proof of Chen's Theorem", arXiv:2203.07871
• Halberstam & Richert, "Sieve Methods" (1974)

1. Local factors

noncomputable def AnalyticNumberTheory.Sieve.localFactor (p N : ℕ) : ℝ

Singular-series local factor at an odd prime p: if p | N, then g(p,N) = (p-1)/(p-2)·(1-1/(p-1)²) = p/(p-1); otherwise g(p,N) = 1-1/(p-1)² = p(p-2)/(p-1)². The prime 2 is treated separately, with factor 2 for even N and factor 1 for odd N in this definition.

Equations

• AnalyticNumberTheory.Sieve.localFactor p N = if p = 2 then if 2 ∣ N then 2 else 1 else if p ∣ N then ↑p / (↑p - 1) else ↑p * (↑p - 2) / (↑p - 1) ^ 2

theorem AnalyticNumberTheory.Sieve.localFactor_two {N : ℕ} (hN : Even N) : localFactor 2 N = 2

The factor at 2 is 2 for even N.

theorem AnalyticNumberTheory.Sieve.localFactor_two_odd {N : ℕ} (hN : Odd N) : localFactor 2 N = 1

The factor at 2 is 1 for odd N.

theorem AnalyticNumberTheory.Sieve.localFactor_of_dvd {p N : ℕ} (_hp : Nat.Prime p) (hp2 : 2 < p) (hpdvd : p ∣ N) : localFactor p N = ↑p / (↑p - 1)

For a prime p > 2 dividing N, the factor is p/(p-1).

theorem AnalyticNumberTheory.Sieve.localFactor_of_not_dvd {p N : ℕ} (_hp : Nat.Prime p) (hp2 : 2 < p) (hpn : ¬p ∣ N) : localFactor p N = ↑p * (↑p - 2) / (↑p - 1) ^ 2

For a prime p > 2 not dividing N, the factor is p(p-2)/(p-1)².

2. Positivity of local factors

theorem AnalyticNumberTheory.Sieve.localFactor_pos {p N : ℕ} (hp : Nat.Prime p) : 0 < localFactor p N

Every prime local factor is positive.

3. Truncated singular series

noncomputable def AnalyticNumberTheory.Sieve.singularSeriesTruncated (N z : ℕ) : ℝ

Truncated local-factor product: 𝔖(N,z) = Π_{p≤z, p.Prime} localFactor p N. The classical infinite product is obtained by a convergence argument as z → ∞, with the normalization of these local factors; that limiting identification is not part of this definition.

Equations

• AnalyticNumberTheory.Sieve.singularSeriesTruncated N z = ∏ p ∈ Finset.range (z + 1) with Nat.Prime p, AnalyticNumberTheory.Sieve.localFactor p N

theorem AnalyticNumberTheory.Sieve.singularSeriesTruncated_pos (N z : ℕ) (_hz : 1 ≤ z) : 0 < singularSeriesTruncated N z

The truncated singular series is positive, since all factors are positive.

4. Finite singular-series proxy

noncomputable def AnalyticNumberTheory.Sieve.singularSeries (N : ℕ) : ℝ

Finite singular-series proxy, truncated at z=N. The classical full series is a limit lim_{z→∞} 𝔖(N,z), requiring an infinite-product convergence argument. Mertens-type estimates such as Σ_{p≤x}1/p ~ log log x are relevant to quantitative singular-series analysis; this definition does not take that limit.

Equations

• AnalyticNumberTheory.Sieve.singularSeries N = AnalyticNumberTheory.Sieve.singularSeriesTruncated N N

theorem AnalyticNumberTheory.Sieve.singularSeries_pos (N : ℕ) (hN : 2 ≤ N) : 0 < singularSeries N

The finite singular-series proxy is positive.

5. Explicit even case

theorem AnalyticNumberTheory.Sieve.singularSeries_even_factor (N : ℕ) (hN : Even N) (_hN2 : 2 ≤ N) : singularSeriesTruncated N 2 = 2

For even N, truncating at 2 gives exactly the factor 2.

6. Upper bounds for local factors

theorem AnalyticNumberTheory.Sieve.localFactor_dvd_le {p N : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) (hpdvd : p ∣ N) : localFactor p N ≤ 3 / 2

For a prime p > 2 dividing N, p/(p-1) ≤ 3/2, since p ≥ 3.

theorem AnalyticNumberTheory.Sieve.localFactor_not_dvd_lt_one {p N : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) (hpn : ¬p ∣ N) : localFactor p N < 1

For a prime p > 2 not dividing N, p(p-2)/(p-1)² < 1, since p ≥ 3.

7. Elementary singular-series bounds

theorem AnalyticNumberTheory.Sieve.telescope_a (n : ℕ) : ∏ k ∈ Finset.range n, (↑k + 1) / (↑k + 2) = 1 / (↑n + 1)

Telescoping product A: ∏_{k<n} (k+1)/(k+2) = 1/(n+1).

theorem AnalyticNumberTheory.Sieve.telescope_b (n : ℕ) : ∏ k ∈ Finset.range n, (↑k + 3) / (↑k + 2) = (↑n + 2) / 2

Telescoping product B: ∏_{k<n} (k+3)/(k+2) = (n+2)/2.

theorem AnalyticNumberTheory.Sieve.int_square_product (N : ℕ) (hN : 2 ≤ N) : ∏ n ∈ Finset.Ico 2 N, (1 - 1 / ↑n ^ 2) = ↑N / (2 * (↑N - 1))

Telescoping product: ∏_{n=2}^{N-1} (1-1/n²) = N/(2(N-1)) for N ≥ 2.

theorem AnalyticNumberTheory.Sieve.prime_square_product_ge_int (N : ℕ) : ∏ n ∈ Finset.Ico 2 N, (1 - 1 / ↑n ^ 2) ≤ ∏ p ∈ Finset.range (N + 1) with Nat.Prime p ∧ 2 < p, (1 - 1 / (↑p - 1) ^ 2)

The prime-indexed product is at least the full integer product: ∏_{3≤p≤N, p prime} (1-1/(p-1)²) ≥ ∏_{n=2}^{N-1} (1-1/n²).

theorem AnalyticNumberTheory.Sieve.singularSeries_bounded_below : ∃ (c : ℝ), 0 < c ∧ ∀ (N : ℕ), 2 ≤ N → Even N → c ≤ singularSeries N

Positive lower bound for even N: the finite proxy is at least 1 for every even N ≥ 2. Its product is 2·∏_{p≤N, p|N, p>2} p/(p-1) ·∏_{p≤N, p∤N, p>2} p(p-2)/(p-1)². The divisor factors are at least 1, and ∏_{2<p≤N}(1-1/(p-1)²) ≥ ∏_{n=2}^{N-1}(1-1/n²) = N/(2(N-1)) ≥ 1/2. Thus the product is at least 2·1·1/2 = 1.

theorem AnalyticNumberTheory.Sieve.singularSeries_bounded_above : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ), 2 ≤ N → singularSeries N ≤ C * ↑N

Upper bound for the finite proxy: for N ≥ 2, the local-factor estimates give 𝔖(N) ≤ 2^{ω(N)} and in particular the stated bound ≤ 2N. Each factor at a prime dividing N is at most 2; the others are at most 1. The coarser 2^{ω(N)+1} ≤ 2N also suffices.

An absolute bound 𝔖(N) ≤ C is false. For primorials N = 2·3·5·7·...·x, the divisor-prime product ∏_{p|N} p/(p-1) has order log log N and is unbounded; the remaining twin-prime-type factors do not remove that growth.

7.5 Uniform lower bound for truncated products

theorem AnalyticNumberTheory.Sieve.singularSeriesTruncated_ge_half (N z : ℕ) (hz : 2 ≤ z) : 1 / 2 ≤ singularSeriesTruncated N z

Uniform truncated-product lower bound: 𝔖(N,z) ≥ 1/2 for every N and z ≥ 2. Write the product as localFactor(2,N)·∏_{2<p≤z} localFactor(p,N). The factor at 2 is at least 1, and for odd primes localFactor(p,N) ≥ 1-1/(p-1)² (the divisor case is at least 1, and the nondivisor case is equality). Therefore 𝔖(N,z) ≥ ∏_{2<p≤z}(1-1/(p-1)²) ≥ ∏_{n=2}^{z-1}(1-1/n²) = z/(2(z-1)) ≥ 1/2. This supplies the twin-prime-constant-scale input c_S = 1/2 for CorrectedChenMainTermLower.

8. Scope and applications