Finite logarithmic bridge for Mertens' product theorem

This module isolates the elementary part of the product argument. The identification of the limiting constant with Euler's constant is deliberately kept separate: it requires an Euler-product/Abelian bridge, rather than only the prime-number theorem.

noncomputable def AnalyticNumberTheory.Mertens.logarithmicCorrection (x : ℕ) : ℝ

The finite quadratic-and-higher correction in the logarithm of the prime Euler product.

Equations

• AnalyticNumberTheory.Mertens.logarithmicCorrection x = ∑ p ∈ AnalyticNumberTheory.Mertens.primesUpTo x, (-Real.log (1 - 1 / ↑p) - 1 / ↑p)

noncomputable def AnalyticNumberTheory.Mertens.logarithmicCorrectionTerm (p : ℕ) : ℝ

The correction term, extended by zero away from the primes so that it can be treated as an ordinary series on ℕ.

Equations

• AnalyticNumberTheory.Mertens.logarithmicCorrectionTerm p = if Nat.Prime p then -Real.log (1 - 1 / ↑p) - 1 / ↑p else 0

noncomputable def AnalyticNumberTheory.Mertens.logarithmicCorrectionLimit : ℝ

The candidate limiting correction constant.

Equations

• AnalyticNumberTheory.Mertens.logarithmicCorrectionLimit = ∑' (p : ℕ), AnalyticNumberTheory.Mertens.logarithmicCorrectionTerm p

theorem AnalyticNumberTheory.Mertens.logarithmicCorrection_eq_sum_range (x : ℕ) : logarithmicCorrection x = ∑ p ∈ Finset.range (x + 1), logarithmicCorrectionTerm p

The filtered finite correction is the initial segment of its zero-extended series.

theorem AnalyticNumberTheory.Mertens.summable_logarithmicCorrectionTerm : Summable logarithmicCorrectionTerm

The zero-extended logarithmic correction is absolutely summable.

theorem AnalyticNumberTheory.Mertens.tendsto_logarithmicCorrection : Filter.Tendsto logarithmicCorrection Filter.atTop (nhds logarithmicCorrectionLimit)

The finite correction converges to its absolutely convergent series.

theorem AnalyticNumberTheory.Mertens.logarithmicCorrectionLimit_sub_eq_tail (x : ℕ) : logarithmicCorrectionLimit - logarithmicCorrection x = ∑' (n : ℕ), logarithmicCorrectionTerm (n + (x + 1))

The difference between the limiting correction and its finite version is the shifted tail of the absolutely convergent series.

theorem AnalyticNumberTheory.Mertens.logarithmicCorrection_tail_norm_le (x : ℕ) : ‖logarithmicCorrectionLimit - logarithmicCorrection x‖ ≤ ∑' (n : ℕ), 2 / ↑(n + (x + 1)) ^ 2

The correction tail is dominated by the corresponding shifted reciprocal square series.

theorem AnalyticNumberTheory.Mertens.shifted_reciprocal_square_tail_le (x : ℕ) (hx : 1 ≤ x) : ∑' (n : ℕ), 2 / ↑(n + (x + 1)) ^ 2 ≤ 2 / ↑x

Integral comparison for the shifted reciprocal-square tail.

theorem AnalyticNumberTheory.Mertens.logarithmicCorrection_tail_norm_le_div (x : ℕ) (hx : 1 ≤ x) : ‖logarithmicCorrectionLimit - logarithmicCorrection x‖ ≤ 2 / ↑x

Explicit O(1/x) bound for the logarithmic correction tail.

theorem AnalyticNumberTheory.Mertens.logarithmicCorrection_tail_isBigO : (fun (n : ℕ) => logarithmicCorrectionLimit - logarithmicCorrection n) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n

On the Mertens scale, the logarithmic correction tail is negligible.

theorem AnalyticNumberTheory.Mertens.neg_log_primeProduct_eq_reciprocal_add_correction (x : ℕ) : -Real.log (primeProduct x) = primeReciprocalSum x + logarithmicCorrection x

Taking the logarithm of the finite Euler product separates the reciprocal prime sum from its convergent higher-order correction.

theorem AnalyticNumberTheory.Mertens.log_primeProduct_error_eq (n : ℕ) : Real.log (primeProduct n) + Real.log (Real.log ↑n) + (mertensSecondConstant + logarithmicCorrectionLimit) = -(primeReciprocalSum n - (Real.log (Real.log ↑n) + mertensSecondConstant)) + (logarithmicCorrectionLimit - logarithmicCorrection n)

The logarithmic product error is the sum of the Mertens-II error and the convergent higher-order correction tail.

theorem AnalyticNumberTheory.Mertens.log_primeProduct_mertens_isBigO : (fun (n : ℕ) => Real.log (primeProduct n) + Real.log (Real.log ↑n) + (mertensSecondConstant + logarithmicCorrectionLimit)) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n

Mertens' product logarithm with its canonical (not yet identified as Euler--Mascheroni) constant.

theorem AnalyticNumberTheory.Mertens.exp_log_primeProduct_error_isBigO : (fun (n : ℕ) => Real.exp (Real.log (primeProduct n) + Real.log (Real.log ↑n) + (mertensSecondConstant + logarithmicCorrectionLimit)) - 1) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n

Exponentiating the canonical logarithmic Mertens error preserves its O(1 / log x) scale. This is the analytic input for the final product-scale O(1 / log² x) estimate.

theorem AnalyticNumberTheory.Mertens.primeProduct_error_eq_canonical_factor (n : ℕ) (hn : 1 < n) : primeProduct n - Real.exp (-(mertensSecondConstant + logarithmicCorrectionLimit)) / Real.log ↑n = Real.exp (-(mertensSecondConstant + logarithmicCorrectionLimit)) / Real.log ↑n * (Real.exp (Real.log (primeProduct n) + Real.log (Real.log ↑n) + (mertensSecondConstant + logarithmicCorrectionLimit)) - 1)

Algebraic factorization converting the exponentiated logarithmic error into the product-scale error, once n > 1.

theorem AnalyticNumberTheory.Mertens.primeProduct_canonical_mertens_isBigO : (fun (n : ℕ) => primeProduct n - Real.exp (-(mertensSecondConstant + logarithmicCorrectionLimit)) / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n ^ 2

Mertens' product formula with the canonical constant supplied by the hard-cutoff proof. Identifying this constant with Euler--Mascheroni is a separate Abelian finite-part theorem.

theorem AnalyticNumberTheory.Mertens.primeProduct_mertens_isBigO_of_constant_eq (hconstant : mertensSecondConstant + logarithmicCorrectionLimit = Real.eulerMascheroniConstant) : (fun (n : ℕ) => primeProduct n - Real.exp (-Real.eulerMascheroniConstant) / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n ^ 2

Once the Abelian finite-part bridge identifies the canonical constant with Euler--Mascheroni, the canonical product estimate becomes the usual Mertens product formula.