Abelian ingredients for Mertens' product theorem

This module keeps the Euler-product continuity argument separate from the hard-cutoff Mertens estimates. The remaining constant-identification bridge will use these ingredients together with an Abelian finite-part lemma.

noncomputable def AnalyticNumberTheory.Mertens.primeEulerCorrection (s : ℝ) (p : Nat.Primes) : ℝ

The quadratic-and-higher Euler-log correction at real exponent s.

Equations

• AnalyticNumberTheory.Mertens.primeEulerCorrection s p = -Real.log (1 - ↑↑p ^ (-s)) - ↑↑p ^ (-s)

theorem AnalyticNumberTheory.Mertens.prime_rpow_neg_le_half (p : Nat.Primes) {s : ℝ} (hs : 1 < s) : ↑↑p ^ (-s) ≤ 1 / 2

Above s = 1, a prime Euler factor is at most one half.

theorem AnalyticNumberTheory.Mertens.norm_primeEulerCorrection_le (p : Nat.Primes) {s : ℝ} (hs : 1 < s) : ‖primeEulerCorrection s p‖ ≤ 2 * ↑↑p ^ (-2)

Uniform quadratic bound for the real Euler-log correction above s = 1.

theorem AnalyticNumberTheory.Mertens.tendsto_primeEulerCorrection (p : Nat.Primes) : Filter.Tendsto (fun (s : ℝ) => primeEulerCorrection s p) (nhdsWithin 1 (Set.Ioi 1)) (nhds (-Real.log (1 - 1 / ↑↑p) - 1 / ↑↑p))

Each real Euler-log correction converges to its s = 1 value.

theorem AnalyticNumberTheory.Mertens.tendsto_tsum_primeEulerCorrection : Filter.Tendsto (fun (s : ℝ) => ∑' (p : Nat.Primes), primeEulerCorrection s p) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∑' (p : Nat.Primes), primeEulerCorrection 1 p))

The absolutely convergent Euler-log correction is continuous as s → 1⁺.

theorem AnalyticNumberTheory.Mertens.tsum_primeEulerCorrection_one : ∑' (p : Nat.Primes), primeEulerCorrection 1 p = logarithmicCorrectionLimit

At s = 1, the prime-indexed Euler correction is the existing zero-extended logarithmic correction constant.

theorem AnalyticNumberTheory.Mertens.tendsto_tsum_primeEulerCorrection_limit : Filter.Tendsto (fun (s : ℝ) => ∑' (p : Nat.Primes), primeEulerCorrection s p) (nhdsWithin 1 (Set.Ioi 1)) (nhds logarithmicCorrectionLimit)

The real Euler-log correction tends to the canonical product correction constant as s → 1⁺.

theorem AnalyticNumberTheory.Mertens.real_primeEulerLog_decomposition {s : ℝ} (hs : 1 < s) : ∑' (p : Nat.Primes), -Real.log (1 - ↑↑p ^ (-s)) = ∑' (p : Nat.Primes), ↑↑p ^ (-s) + ∑' (p : Nat.Primes), primeEulerCorrection s p

For a real exponent above one, the Euler logarithm splits into its prime Dirichlet term and the uniformly convergent higher-order correction.

theorem AnalyticNumberTheory.Mertens.complex_integral_log_mul_exp_eq_neg_eulerMascheroni : ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (1 - 1) * (↑(Real.log t) * ↑(Real.exp (-t))) = -↑Real.eulerMascheroniConstant

The Gamma kernel responsible for the Euler--Mascheroni constant in the Abelian finite-part calculation.

theorem AnalyticNumberTheory.Mertens.complex_integral_log_exp_eq_neg_eulerMascheroni : ∫ (t : ℝ) in Set.Ioi 0, ↑(Real.log t) * ↑(Real.exp (-t)) = -↑Real.eulerMascheroniConstant

Simplified Gamma kernel form used by the Mellin finite-part calculation.