Documentation

AnalyticNumberTheory.Mertens.Abelian

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.

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

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

Equations
Instances For
    source
    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.

    source
    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.

    source
    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.

    source
    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⁺.

    source
    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.

    source
    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⁺.

    source
    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.

    source
    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.

    source
    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.