MathlibNt.SieveTheory.MertensTheorem

Mertens' theorems

Mertens' theorems provide the basis for estimates of the sieve product V(z) and its relation to the singular series 𝔖(N) in Chen's theorem.

Mertens' second theorem: there is a constant B₁ such that Σ_{p ≤ x} 1/p = log log x + B₁ + O(1/log x).

Mertens' product formula: Π_{p ≤ x} (1 - 1/p) ~ e^(-γ) / log x, where γ is the Euler-Mascheroni constant.

Applications to Chen's theorem:

• V(z) = Π_{p < z, p ∤ N} (1 - ν(p)/p) ≈ 𝔖(N) · e^(-γ) / log z in the classical notation for the sieve density;
• the convergent product Π_{p > 2} (1 - 1/(p-1)²), the twin-prime constant, controls the odd-prime factors not dividing N. This does not give an absolute upper bound on 𝔖(N) uniform in N.

The exact finite identity below uses singularSeriesTruncated N (z - 1); both its main term and its error term retain this factor.

References:

• Chen, J.R. (1973), Sci. Sinica 16, 157-176
• Liu, Z. (2022), arXiv:2203.07871, Lemma 1
• Nathanson, "Additive Number Theory", GTM 164

1. Mertens' second theorem

noncomputable def MathlibNt.SieveTheory.MertensTheorem.primeReciprocalSum (x : ℕ) : ℝ

The sum of prime reciprocals: Σ_{p ≤ x} 1/p.

Equations

• MathlibNt.SieveTheory.MertensTheorem.primeReciprocalSum x = ∑ p ∈ Finset.range (x + 1) with Nat.Prime p, 1 / ↑p

theorem MathlibNt.SieveTheory.MertensTheorem.primeReciprocalSum_eq_analyticNumberTheory (x : ℕ) : primeReciprocalSum x = AnalyticNumberTheory.Mertens.primeReciprocalSum x

The Chen-local reciprocal sum is definitionally the reusable ANT object.

theorem MathlibNt.SieveTheory.MertensTheorem.mertens_second_theorem : ∃ (B₁ : ℝ) (C : ℝ), ∀ (x : ℕ), 2 ≤ x → |primeReciprocalSum x - (Real.log (Real.log ↑x) + B₁)| ≤ C / Real.log ↑x

Mertens' second theorem: there is a constant B₁ such that Σ_{p ≤ x} 1/p = log log x + B₁ + O(1/log x)

This underlies Lemma 1 in the proof of Chen's theorem. One possible proof uses the prime number theorem and Abel summation, but the PNT is not necessary: Mertens' theorem also has elementary proofs.

Smooth weights on logarithmic prime intervals

noncomputable def MathlibNt.SieveTheory.MertensTheorem.rpowFloor (N : ℕ) (a : ℝ) : ℕ

The floor of the real power used as an exact natural cutoff.

Equations

• MathlibNt.SieveTheory.MertensTheorem.rpowFloor N a = ⌊↑N ^ a⌋₊

noncomputable def MathlibNt.SieveTheory.MertensTheorem.weightedPrimeReciprocalLogSum (f : ℝ → ℝ) (N : ℕ) (a b : ℝ) : ℝ

The reciprocal-prime sum with a test function on logarithmic scale.

The Ioc endpoints are literal floors of the real powers. Thus, when N ≥ 1, membership is exactly N ^ a < p ∧ p ≤ N ^ b; no endpoint error is hidden in the definition.

Equations

• MathlibNt.SieveTheory.MertensTheorem.weightedPrimeReciprocalLogSum f N a b = ∑ p ∈ Finset.Ioc (MathlibNt.SieveTheory.MertensTheorem.rpowFloor N a) (MathlibNt.SieveTheory.MertensTheorem.rpowFloor N b) with Nat.Prime p, f (Real.log ↑p / Real.log ↑N) / ↑p

theorem MathlibNt.SieveTheory.MertensTheorem.mem_Ioc_rpowFloor_iff {N p : ℕ} {a b : ℝ} : p ∈ Finset.Ioc (rpowFloor N a) (rpowFloor N b) ↔ ↑N ^ a < ↑p ∧ ↑p ≤ ↑N ^ b

The floor cutoffs encode the intended half-open real-power interval exactly.

theorem MathlibNt.SieveTheory.MertensTheorem.weightedPrimeReciprocalLogSum_eq_sub_sub_integral {a b : ℝ} (_ha : 0 < a) (hab : a ≤ b) {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : Continuous f') {N : ℕ} (hN : 1 < N) : weightedPrimeReciprocalLogSum f N a b = f b * primeReciprocalSum (rpowFloor N b) - f a * primeReciprocalSum (rpowFloor N a) - ∫ (t : ℝ) in Set.Ioc (↑N ^ a) (↑N ^ b), MathlibNt.SieveTheory.MertensTheorem.logScaleDeriv✝ f' N t * primeReciprocalSum ⌊t⌋₊

Finite Abel summation for a logarithmically rescaled smooth test function. This is an exact identity, including both floored real-power endpoints.

theorem MathlibNt.SieveTheory.MertensTheorem.tendsto_weightedPrimeReciprocalLogSum_const {a b c : ℝ} (ha : 0 < a) (hab : a < b) : Filter.Tendsto (fun (N : ℕ) => weightedPrimeReciprocalLogSum (fun (x : ℝ) => c) N a b) Filter.atTop (nhds (c * Real.log (b / a)))

For a constant test function, the exact real-power prime interval has the expected logarithmic limit. This is the base case for finite-step approximations of general continuous test functions.

theorem MathlibNt.SieveTheory.MertensTheorem.tendsto_finset_weightedPrimeReciprocalLogSum_const {ι : Type u_1} (s : Finset ι) (c a b : ι → ℝ) (ha : ∀ i ∈ s, 0 < a i) (hab : ∀ i ∈ s, a i < b i) : Filter.Tendsto (fun (N : ℕ) => ∑ i ∈ s, weightedPrimeReciprocalLogSum (fun (x : ℝ) => c i) N (a i) (b i)) Filter.atTop (nhds (∑ i ∈ s, c i * Real.log (b i / a i)))

A fixed finite linear combination of constant logarithmic cells converges to the same linear combination of logarithmic masses.

theorem MathlibNt.SieveTheory.MertensTheorem.tendsto_weightedPrimeReciprocalLogSum_of_hasDerivAt {a b : ℝ} (ha : 0 < a) (hab : a < b) {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : Continuous f') : Filter.Tendsto (fun (N : ℕ) => weightedPrimeReciprocalLogSum f N a b) Filter.atTop (nhds (∫ (x : ℝ) in a..b, f x / x))

A continuously differentiable test function on a fixed positive logarithmic interval has the expected Mertens-weighted prime-sum limit. The sum uses the literal floored cutoffs ⌊N ^ a⌋ and ⌊N ^ b⌋.

theorem MathlibNt.SieveTheory.MertensTheorem.tendsto_weightedPrimeReciprocalLogSum {a b : ℝ} (ha : 0 < a) (hab : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : Filter.Tendsto (fun (N : ℕ) => weightedPrimeReciprocalLogSum f N a b) Filter.atTop (nhds (∫ (x : ℝ) in a..b, f x / x))

A continuous test function on a fixed positive logarithmic interval has the expected reciprocal-prime limit.

2. Mertens' product formula

noncomputable def MathlibNt.SieveTheory.MertensTheorem.primeProduct (x : ℕ) : ℝ

The prime product: Π_{p ≤ x} (1 - 1/p).

Equations

• MathlibNt.SieveTheory.MertensTheorem.primeProduct x = ∏ p ∈ Finset.range (x + 1) with Nat.Prime p, (1 - 1 / ↑p)

theorem MathlibNt.SieveTheory.MertensTheorem.primeProduct_eq_analyticNumberTheory (x : ℕ) : primeProduct x = AnalyticNumberTheory.Mertens.primeProduct x

The Chen-local Euler product is definitionally the reusable ANT object.

theorem MathlibNt.SieveTheory.MertensTheorem.mertens_product_formula : ∃ (C : ℝ), ∀ (x : ℕ), 2 ≤ x → |primeProduct x - Real.exp (-Real.eulerMascheroniConstant) / Real.log ↑x| ≤ C / Real.log ↑x ^ 2

Mertens' product formula: Π_{p ≤ x} (1 - 1/p) ~ e^(-γ) / log x.

The quantitative form here gives a constant C such that |Π_{p ≤ x} (1 - 1/p) - e^(-γ) / log x| ≤ C / (log x)².

This is a central tool for estimating V(z).

theorem MathlibNt.SieveTheory.MertensTheorem.primeProduct_asymptotic_order : ∃ (c₁ : ℝ) (c₂ : ℝ), 0 < c₁ ∧ ∀ (x : ℕ), 2 ≤ x → c₁ / Real.log ↑x ≤ primeProduct x ∧ primeProduct x ≤ c₂ / Real.log ↑x

Order form of Mertens' product formula: primeProduct x = Θ(1/log x); there are positive constants c₁, c₂ such that c₁/log x ≤ Π_{p ≤ x}(1 - 1/p) ≤ c₂/log x.

This weaker version of mertens_product_formula, which has the exact constant e^{-γ}, follows directly from Mertens' second theorem via -log Π = Σ 1/p + O(1). It does not require the Euler-Mascheroni constant identity. Proof outline:

1. log Π = Σ log(1 - 1/p), and |log(1 - 1/p) + 1/p| ≤ 2/p².
2. Thus -log Π = Σ 1/p + E(x), with |E(x)| ≤ Σ 2/p² ≤ 2·Σ_{n≥1} 1/n² < ∞.
3. Mertens' second theorem gives Σ 1/p = log log x + B₁ + O(1/log x).
4. Hence Π = exp(-B₁ - δ - E)/log x, where |δ| and |E| are bounded, so Π = Θ(1/log x).

3. Application: bounded prime-reciprocal sums (Lemma 1)

theorem MathlibNt.SieveTheory.MertensTheorem.primeProduct_lower_bound : ∃ (cpp : ℝ), 0 < cpp ∧ ∀ (m : ℕ), 3 ≤ m → cpp / Real.log ↑m ≤ primeProduct m

Mertens product lower bound: there is cpp > 0 such that, for every m ≥ 3, cpp / log m ≤ primeProduct m.

This follows directly from primeProduct_asymptotic_order, which gives c₁/log x ≤ primeProduct x for every x ≥ 2. It is one of the two standard inputs to the main-term lower bound CorrectedChenMainTermLower.

theorem MathlibNt.SieveTheory.MertensTheorem.primeProduct_lower_bound_exists : ∃ (cpp : ℝ), 0 < cpp ∧ ∀ (m : ℕ), 3 ≤ m → cpp / Real.log ↑m ≤ primeProduct m

Existentially named form of primeProduct_lower_bound, for clients that choose a fixed lower-bound constant.

theorem MathlibNt.SieveTheory.MertensTheorem.prime_reciprocal_sum_bounded (α β : ℝ) (hα : 0 < α) (_hβ : α < β) : ∃ (C : ℝ), ∀ (x : ℕ), 2 ≤ x → |∑ p ∈ Finset.range (x + 1) with Nat.Prime p ∧ ↑x ^ α < ↑p ∧ ↑p ≤ ↑x ^ β, 1 / ↑p| ≤ C

Lemma 1 (Liu 2022): for fixed 0 < α < β, the sum Σ_{x^α < p ≤ x^β} 1/p is bounded.

By Mertens' second theorem, Σ_{x^α < p ≤ x^β} 1/p = (log log x^β + B₁ + O(1/log x)) - (log log x^α + B₁ + O(1/log x)) = log(β/α) + O(1/log x)

Thus the sum is bounded, as is the further truncation to p ≤ x used here.

4. Application: an asymptotic formula for the sieve product V(z)

noncomputable def MathlibNt.SieveTheory.MertensTheorem.goldbachSieveProduct (N z : ℕ) : ℝ

Goldbach sieve product V(z, N) = Π_{p < z, p ∤ N} (1 - 1/(p-1)).

Equations

• MathlibNt.SieveTheory.MertensTheorem.goldbachSieveProduct N z = ∏ p ∈ Finset.range z with Nat.Prime p ∧ ¬p ∣ N, (1 - 1 / (↑p - 1))

theorem MathlibNt.SieveTheory.MertensTheorem.goldbachSieveProduct_lower_bound : ∃ (c₁ : ℝ), 0 < c₁ ∧ ∀ (N z : ℕ), 2 ≤ z → Even N → 4 ≤ N → c₁ / Real.log ↑z ≤ goldbachSieveProduct N z

Sieve-product lower bound: there is c₁ > 0 such that, for every even N ≥ 4 and z ≥ 2, c₁ / log z ≤ V(z, N) = Π_{p < z, p ∤ N}(1 - 1/(p-1)).

Proof outline:

1. Evenness of N excludes p = 2 from the sieve product. Omitting factors with p | N can only increase the product, so V ≥ W(z) := Π_{p < z, p > 2}(1 - 1/(p-1)).
2. Use the local correction |log(1 - 1/(p-1)) + 1/(p-1)| ≤ 2/(p-1)².
3. By Mertens' second theorem, -log W = Σ_{p<z,p>2} 1/(p-1) + O(1) ≤ log log z + O(1).
4. Exponentiating gives W = exp(log W) ≥ e^{-C}/log z.

This supplies the lower-bound scale in V ≈ 𝔖(N)·e^{-γ}/log z, as needed for the Jurkat-Richert main term.

theorem MathlibNt.SieveTheory.MertensTheorem.goldbachSieveProduct_le_one (N z : ℕ) : goldbachSieveProduct N z ≤ 1

Sieve-product upper bound: V(z, N) ≤ 1, since every factor lies in [0, 1]. The factor at p = 2 can be zero when N is odd.

theorem MathlibNt.SieveTheory.MertensTheorem.sieveProduct_identity (N z : ℕ) (hz : 2 ≤ z) (hN : Even N) : goldbachSieveProduct N z = primeProduct (z - 1) * SingularSeries.singularSeriesTruncated N (z - 1)

Sieve-product identity: V(z,N) = Π_{p<z}(1-1/p) · 𝔖(N,z-1).

For odd primes, factor (1-1/(p-1)) = (1-1/p)(1-1/(p-1)²). Then:

• if p ∤ N (which excludes p = 2 for even N), (1-1/p)·localFactor(p,N) = 1-1/(p-1);
• if p | N (including p = 2, since N is even), (1-1/p)·localFactor(p,N) = 1. Thus Π_{p<z}(1-1/p)·𝔖(N,z-1) = Π_{p<z}[(1-1/p)·localFactor(p,N)] = V.

This is the exact identity underlying V ≈ 𝔖(N)·e^{-γ}/log z.

theorem MathlibNt.SieveTheory.MertensTheorem.sieveProduct_order : ∃ (c₁ : ℝ) (c₂ : ℝ), 0 < c₁ ∧ ∀ (N z : ℕ), 3 ≤ z → Even N → 4 ≤ N → c₁ * SingularSeries.singularSeriesTruncated N (z - 1) / Real.log ↑z ≤ goldbachSieveProduct N z ∧ goldbachSieveProduct N z ≤ c₂ * SingularSeries.singularSeriesTruncated N (z - 1) / Real.log ↑z

Order of the sieve product: there are c₁, c₂ > 0 such that, for every even N ≥ 4 and z ≥ 3, c₁·𝔖(N,z-1)/log z ≤ V(z,N) ≤ c₂·𝔖(N,z-1)/log z.

This follows directly from V = Π_{p<z}(1-1/p)·𝔖(N,z-1) and primeProduct_asymptotic_order, which gives Π_{p<z}(1-1/p) = Θ(1/log z).

4.5 Sums of 1/(p-1) over primes (for Selberg Lemma 2)

theorem MathlibNt.SieveTheory.MertensTheorem.prime_inv_sq_bound : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (y : ℕ), ∑ p ∈ Finset.range (y + 1) with Nat.Prime p, 1 / ↑p ^ 2 ≤ K

Σ_{p ≤ y} 1/p² is bounded by a constant depending only on Σ_{n≥1} 1/n².

theorem MathlibNt.SieveTheory.MertensTheorem.prime_inv_pminus1_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℕ), 3 ≤ y → ∑ p ∈ Finset.range (y + 1) with Nat.Prime p, 1 / (↑p - 1) ≤ Real.log (Real.log ↑y) + C

Σ_{p ≤ y} 1/(p-1) ≤ log(log y) + C for y ≥ 3, by Mertens' second theorem and a decomposition of each summand.

theorem MathlibNt.SieveTheory.MertensTheorem.sieve_product_asymptotic : ∃ (C : ℝ), ∀ (N z : ℕ), 3 ≤ z → Even N → 4 ≤ N → |goldbachSieveProduct N z - SingularSeries.singularSeriesTruncated N (z - 1) * Real.exp (-Real.eulerMascheroniConstant) / Real.log ↑(z - 1)| ≤ C * SingularSeries.singularSeriesTruncated N (z - 1) / Real.log ↑(z - 1) ^ 2

Sieve-product asymptotic formula: V(z, N) ≈ 𝔖(N, z-1) · e^(-γ) / log(z-1).

Here 𝔖(N, z) = Π_{p ≤ z, p.Prime} localFactor(p, N) is the truncated singular series (SingularSeries.singularSeriesTruncated).

The singular-series factor cannot be omitted: N with many small odd prime factors contribute local corrections p/(p-1) that are not uniformly bounded. The asymptotic V ≈ 𝔖(N)·e^{-γ}/log z follows from (1 - 1/(p-1)) = (1 - 1/p)·(1 - 1/(p-1)²) at odd primes and Mertens' product formula. It underlies the calculation of the Jurkat-Richert main term X · V(z).

The error must also be multiplied by the truncated singular series to obtain a consequence of Mertens' product formula uniform in N. The cutoff z - 1 corresponds exactly to the range p < z in goldbachSieveProduct.

5. Auxiliary lemmas: the prime-counting function

def MathlibNt.SieveTheory.MertensTheorem.primeCount (x : ℕ) : ℕ

Prime-counting function π(x) = |{p ≤ x : p prime}|.

Equations

• MathlibNt.SieveTheory.MertensTheorem.primeCount x = (Finset.filter Nat.Prime (Finset.range (x + 1))).card

theorem MathlibNt.SieveTheory.MertensTheorem.primeCount_eq_primeCounting (x : ℕ) : primeCount x = x.primeCounting

The project's finite prime count agrees definitionally with mathlib's Nat.primeCounting. This is the normalization needed when importing a PNT stated using mathlib's standard counting function.

def MathlibNt.SieveTheory.MertensTheorem.PrimeCountingPNT : Prop

A prime-counting PNT in the normal form exported by PNTAnd's pi_alt.

This is kept as a separate interface: adapting an external proof to the project toolchain only has to establish this proposition.

Equations

• MathlibNt.SieveTheory.MertensTheorem.PrimeCountingPNT = ∃ (c : ℕ → ℝ), (c =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ (x : ℕ), ↑(MathlibNt.SieveTheory.MertensTheorem.primeCount x) = (1 + c x) * ↑x / Real.log ↑x

theorem MathlibNt.SieveTheory.MertensTheorem.primeCountingPNT_implies_prime_number_theorem (hPNT : PrimeCountingPNT) (ε : ℝ) : 0 < ε → ∃ (x₀ : ℕ), ∀ (x : ℕ), x₀ ≤ x → |↑(primeCount x) - ↑x / Real.log ↑x| ≤ ε * ↑x / Real.log ↑x

The pi_alt normal form implies the epsilon formulation used by the project's PNT declaration.

theorem MathlibNt.SieveTheory.MertensTheorem.primeCount_pos (x : ℕ) (hx : 2 ≤ x) : 0 < primeCount x

π(x) ≥ 1 for x ≥ 2, since the prime 2 is counted.

theorem MathlibNt.SieveTheory.MertensTheorem.prime_number_theorem (ε : ℝ) : 0 < ε → ∃ (x₀ : ℕ), ∀ (x : ℕ), x₀ ≤ x → |↑(primeCount x) - ↑x / Real.log ↑x| ≤ ε * ↑x / Real.log ↑x

Prime number theorem (PNT): π(x) ~ x / log x.

That is, |π(x) - x/log x| / (x/log x) → 0 as x → ∞. The PNT provides one possible route to Mertens' theorems, though elementary proofs are also available.

6. The twin-prime constant and a finite truncation

noncomputable def MathlibNt.SieveTheory.MertensTheorem.twinPrimeConstant : ℝ

Legacy finite truncation of the twin-prime Euler product.

This is a working finite product, not the canonical infinite twin-prime constant, and it is not used to justify the canonical Chen endpoint.

Equations

• MathlibNt.SieveTheory.MertensTheorem.twinPrimeConstant = ∏ p ∈ Finset.range 100 with Nat.Prime p ∧ 2 < p, (1 - 1 / (↑p - 1) ^ 2)

theorem MathlibNt.SieveTheory.MertensTheorem.twinPrimeConstant_pos : 0 < twinPrimeConstant

The legacy finite twin-prime product is positive because each factor is positive.

theorem MathlibNt.SieveTheory.MertensTheorem.twinPrimeConstant_lt_one : twinPrimeConstant < 1

The finite twin-prime product is less than 1: every factor is in (0, 1), and the factor at p = 3 is 3/4 < 1.

6.5 Local interval factors

theorem MathlibNt.SieveTheory.MertensTheorem.exists_log_goldbach_inverse_interval_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (k n : ℕ), 2 ≤ k → k ≤ n → ∀ (s : Finset ℕ), (∀ p ∈ s, Nat.Prime p ∧ k < p ∧ p ≤ n) → Real.log (∏ p ∈ s, (1 - 1 / (↑p - 1))⁻¹) ≤ Real.log (Real.log ↑n / Real.log ↑k) + (2 * C + 24) / Real.log ↑k

A quantitative interval form of Mertens' second theorem for inverse Goldbach local factors. The error has the sharp inverse-logarithmic shape needed by the dimension-one sieve hypothesis.

theorem MathlibNt.SieveTheory.MertensTheorem.exists_goldbach_inverse_interval_bound : ∃ (K : ℝ), 1 < K ∧ ∀ (s : Finset ℕ), (∀ p ∈ s, Nat.Prime p ∧ 2 < p) → ∀ (z₁ z₂ : ℝ), 2 ≤ z₁ → z₁ ≤ z₂ → (∀ p ∈ s, z₁ ≤ ↑p ∧ ↑p < z₂) → ∏ p ∈ s, (1 - 1 / (↑p - 1))⁻¹ ≤ Real.log z₂ / Real.log z₁ * (1 + K / Real.log z₁)

The inverse Goldbach local factors on an arbitrary real interval satisfy the standard dimension-one product bound.

7. Mathematical scope