Documentation

AnalyticNumberTheory.Mertens.FinitePart

The prime Dirichlet finite part #

This module applies Mertens' second theorem to the exponential Abel kernel. It identifies the finite part of the prime Dirichlet series at s = 1 and thereby identifies the canonical product constant with Euler's constant.

source
noncomputable def AnalyticNumberTheory.Mertens.primeAbelRemainder (u : ℝ) :
ℂ

The Mertens-II error after the logarithmic substitution x = exp u.

Equations
Instances For
    source
    theorem AnalyticNumberTheory.Mertens.stronglyMeasurable_primeAbelRemainder :
    MeasureTheory.StronglyMeasurable primeAbelRemainder
    source
    theorem AnalyticNumberTheory.Mertens.primeAbelRemainder_eventually_inv_bound :
    ∃ C > 0, ∀ᶠ (u : ℝ) in Filter.atTop, ‖primeAbelRemainder u‖ ≤ C / u

    Mertens II becomes an O(1/u) bound after x = exp u.

    source
    theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_norm_div_Ioc {A : ℝ} (hA : 1 ≤ A) :
    MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖primeAbelRemainder u‖ / u) (Set.Ioc 1 A) MeasureTheory.volume
    source
    theorem AnalyticNumberTheory.Mertens.tendsto_primeAbelRemainder_tail :
    Filter.Tendsto (fun (ε : ℝ) => ↑ε * ∫ (u : ℝ) in Set.Ioi 1, primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

    The tail of the concrete Mertens-II remainder vanishes under Abel damping.

    source
    theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_norm_div_Ioi_one :
    MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖primeAbelRemainder u‖ / u) (Set.Ioi 1) MeasureTheory.volume
    source
    theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_mul_exp_tail (ε : ℝ) (hε : 0 < ε) :
    MeasureTheory.IntegrableOn (fun (u : ℝ) => primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (Set.Ioi 1) MeasureTheory.volume
    source
    theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_Ioc_zero_one :
    MeasureTheory.IntegrableOn primeAbelRemainder (Set.Ioc 0 1) MeasureTheory.volume

    The logarithmic singularity of the remainder is integrable near zero.

    source
    theorem AnalyticNumberTheory.Mertens.tendsto_primeAbelRemainder_initial :
    Filter.Tendsto (fun (ε : ℝ) => ↑ε * ∫ (u : ℝ) in Set.Ioc 0 1, primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
    source
    theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_mul_exp_initial (ε : ℝ) :
    MeasureTheory.IntegrableOn (fun (u : ℝ) => primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (Set.Ioc 0 1) MeasureTheory.volume
    source
    theorem AnalyticNumberTheory.Mertens.tendsto_primeAbelRemainder_full :
    Filter.Tendsto (fun (ε : ℝ) => ↑ε * ∫ (u : ℝ) in Set.Ioi 0, primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

    The full Mertens-II remainder vanishes under Abel damping.

    source
    theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_mul_exp_full (ε : ℝ) (hε : 0 < ε) :
    MeasureTheory.IntegrableOn (fun (u : ℝ) => primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (Set.Ioi 0) MeasureTheory.volume
    source
    theorem AnalyticNumberTheory.Mertens.primeAbel_integral_finitePart_identity (ε : ℝ) (hε : 0 < ε) :
    (↑ε * ∫ (u : ℝ) in Set.Ioi 0, ↑(primeReciprocalSum ⌊Real.exp u⌋₊) * ↑(Real.exp (-(ε * u)))) + ↑(Real.log ε) = -↑Real.eulerMascheroniConstant + ↑mertensSecondConstant + ↑ε * ∫ (u : ℝ) in Set.Ioi 0, primeAbelRemainder u * ↑(Real.exp (-(ε * u)))

    Exact decomposition of the prime Abel integral into Gamma, constant, and vanishing-remainder terms.

    source
    theorem AnalyticNumberTheory.Mertens.tendsto_primeDirichlet_finitePart :
    Filter.Tendsto (fun (ε : ℝ) => ∑' (p : Nat.Primes), ↑↑p ^ (-(1 + ε)) + Real.log ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds (mertensSecondConstant - Real.eulerMascheroniConstant))

    Abelian finite part of the prime Dirichlet series at s = 1.

    source
    theorem AnalyticNumberTheory.Mertens.mertensConstant_eq_eulerMascheroni :
    mertensSecondConstant + logarithmicCorrectionLimit = Real.eulerMascheroniConstant

    The canonical Mertens product constant is the Euler--Mascheroni constant.