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.

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

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

Equations

• AnalyticNumberTheory.Mertens.primeAbelRemainder u = ↑(AnalyticNumberTheory.Mertens.primeReciprocalSum ⌊Real.exp u⌋₊) - ↑(Real.log u + AnalyticNumberTheory.Mertens.mertensSecondConstant)

theorem AnalyticNumberTheory.Mertens.stronglyMeasurable_primeAbelRemainder : MeasureTheory.StronglyMeasurable primeAbelRemainder

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.

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

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.

theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_norm_div_Ioi_one : MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖primeAbelRemainder u‖ / u) (Set.Ioi 1) MeasureTheory.volume

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

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.

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)

theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_mul_exp_initial (ε : ℝ) : MeasureTheory.IntegrableOn (fun (u : ℝ) => primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (Set.Ioc 0 1) MeasureTheory.volume

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.

theorem AnalyticNumberTheory.Mertens.integrableOn_primeAbelRemainder_mul_exp_full (ε : ℝ) (hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (u : ℝ) => primeAbelRemainder u * ↑(Real.exp (-(ε * u)))) (Set.Ioi 0) MeasureTheory.volume

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.

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.

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

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