Constant identification from the prime finite part #
This module closes the zeta/Euler-product side of the Mertens constant calculation. The only remaining analytic input is the Abelian finite-part limit for the prime Dirichlet series.
theorem
AnalyticNumberTheory.Mertens.mertensConstant_eq_eulerMascheroni_of_primeFinitePart
(hfinite :
Filter.Tendsto (fun (ε : ℝ) => ∑' (p : Nat.Primes), ↑↑p ^ (-(1 + ε)) + Real.log ε) (nhdsWithin 0 (Set.Ioi 0))
(nhds (mertensSecondConstant - Real.eulerMascheroniConstant)))
:
Once the prime Dirichlet finite part is identified as B - γ, the
normalized zeta limit and the convergent Euler correction force B + C = γ.
Inspect dependencies
AnalyticNumberTheory.Mertens.mertensConstant_eq_eulerMascheroni_of_primeFinitePart · compiled type and proof/definition references.