feat(NumberTheory/Mertens): the Mertens theorems

[teorth]

Establish all three of Mertens' theorems, controlling sums and products involving either primes or the von Mangoldt function, with explicit bounds on error terms. This is done by first developing an abstract theory of Mertens weights: functions f : ℕ → ℝ whose partial sums grow like the logarithm function. This is set up through a bundled class Mertens.Weight. Two objects of this type are constructed: Mertens.Weight.vonMangoldt, which bundles the function n ↦ Λ n / n, and Mertens.Weight.prime, which bundles the function n ↦ if n.Prime then log n / n else 0.

---

There are many versions of each of the three theorems provided, but a sample is given here:

• Sample first theorem abs_sum_log_prime_div_sub_le_nat : |∑ p ∈ primesLE N, log p / p - log N| ≤ 2
• Sample second theorem sum_vonMangoldt_div_mul_log_sub_sub_isBigO: (fun x ↦ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n / (n * log n) - log (log x) - eulerMascheroniConstant) =O[atTop] fun x ↦ (log x)⁻¹
• Sample third theorem prod_prime_one_minus_inv_asymp: (fun x ↦ ∏ p ∈ primesLE ⌊x⌋₊, (1 - (1 : ℝ) / p)) ~[atTop] (fun x ↦ exp (-eulerMascheroniConstant) / log x)

This PR supersedes #40656.

The code was human-generated, but reviewed by AI.

Some related estimates on the partial sums of the logarithm function are also included in this file (they are needed to construct the Mertens weights).

• depends on: feat(Analysis): integral test for infinite sums #40588
• depends on: feat(Analysis/Complex/ExponentialBounds): add log 4 and log 10 lemmas #40721
• depends on: feat(Analysis/SpecialFunctions/Log/InvLog): add more API for inv_log and log_log #40847
• depends on: feat(NumberTheory/EulerProduct/DirichletLSeries): establish Dirichlet series for log of L-functions or Riemann-zeta #41097
• depends on: feat(Analysis/SpecialFunctions/Gamma/Deriv,NumberTheory/Harmonic/GammaDeriv): formulae for the derivative of Gamma / eulerMascheroni #41120
• depends on: feat(Topology/Algebra/Group/Basic,Algebra/Group/Pointwise/Set/Basic): add Filter.map_{sub,div}{Left,Right}_nhds{,LT,GT,NE} #41376

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[github-actions]

PR summary 363bdfef77

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Complex.ExponentialBounds	1979	2010	+31 (+1.57%)
Mathlib.Analysis.SpecialFunctions.Gamma.Deriv	2558	2567	+9 (+0.35%)

Import changes for all files

Files	Import difference
145 files Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.ValueDistribution.Cartan Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.Sobolev Mathlib.Analysis.Distribution.Support Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Ring.InfiniteProd Mathlib.Analysis.ODE.ExistUnique Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.Real.Pi.Irrational Mathlib.Analysis.Real.Pi.Leibniz Mathlib.Analysis.Real.Pi.Wallis Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals.Basic Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SumIntegralExpDecay Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion Mathlib.MeasureTheory.Measure.CharacteristicFunction Mathlib.MeasureTheory.Measure.FiniteMeasureExt Mathlib.MeasureTheory.Measure.IntegralCharFun Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.CuspFormSubmodule Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Probability.BrownianMotion.Basic Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Cauchy Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Independence.CharacteristicFunction Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted	1
Mathlib.Analysis.SpecialFunctions.Gamma.Deriv	9
Mathlib.Analysis.Complex.ExponentialBounds	31
Mathlib.NumberTheory.Mertens (new file)	3519

---

Declarations diff (regex)

+ AntitoneOn.sum_range_le_integral
+ AntitoneOn.summable_of_integrable
+ AntitoneOn.tsum_add_one_le_integral
+ AntitoneOn.tsum_le_integral
+ C₀_nonneg
+ C₁
+ C₁_nonneg
+ C₂
+ C₂_nonneg
+ DirichletCharacter.LSeries_eq_exp_LSeries
+ DirichletCharacter.eulerProduct_log_eq_LSeries
+ E₁_bound
+ E₁_le
+ E₁_nonneg
+ E₂
+ E₂_bound
+ E₂_bound_weak
+ E₂_eq
+ E₃
+ E₃_bound
+ E₃_isBigO
+ E₃_isLittleO
+ E₃_tendsto
+ Filter.map_divLeft_nhds
+ Filter.map_divLeft_nhdsGT
+ Filter.map_divLeft_nhdsLT
+ Filter.map_divLeft_nhdsNE
+ Filter.map_divRight_nhds
+ Filter.map_divRight_nhdsGT
+ Filter.map_divRight_nhdsLT
+ Filter.map_divRight_nhdsNE
+ Homeomorph.coe_divLeft
+ Homeomorph.coe_divRight
+ LSeries_def₀
+ M
+ M_bounds
+ Weight
+ Weight.prime
+ Weight.prime_C₁_eq
+ Weight.prime_C₂_eq
+ Weight.prime_M_eq
+ Weight.prime_apply
+ Weight.prime_lowerBound_eq
+ Weight.prime_sum_inv_log_mul_eq
+ Weight.prime_upperBound_eq
+ Weight.vonMangoldt
+ Weight.vonMangoldt_C₁_eq
+ Weight.vonMangoldt_C₂_eq
+ Weight.vonMangoldt_M_eq
+ Weight.vonMangoldt_apply
+ Weight.vonMangoldt_lowerBound_eq
+ Weight.vonMangoldt_sum_inv_log_mul_eq
+ Weight.vonMangoldt_upperBound_eq
+ abs_sum_log_prime_div_sub_le
+ abs_sum_log_prime_div_sub_le_nat
+ abs_sum_vonMangoldt_div_sub_le
+ abs_sum_vonMangoldt_div_sub_le_nat
+ apply_bound
+ deriv_Gamma_one_eq_integral_log
+ deriv_Gamma_one_eq_integral_log_log
+ deriv_inv_log'
+ deriv_log_log
+ differentiableAt_inv_log
+ differentiableAt_log_log
+ differentiableOn_inv_log
+ differentiableOn_log_log
+ error
+ eulerMascheroniConstant_eq_neg_integral_log
+ eulerMascheroniConstant_eq_neg_integral_log_log
+ exp_E₃_sub_isBigO
+ exp_E₃_sub_isLittleO
+ exp_E₃_tendsto
+ e₁
+ e₁_nonneg
+ e₁_summable
+ first_le
+ hasDerivAt_inv_log
+ hasDerivAt_log_log
+ hasSum_taylorSeries_neg_log'
+ hi_nonneg
+ image_div_left
+ image_div_right
+ image_exp_Icc
+ image_exp_Ici
+ image_exp_Ico
+ image_exp_Ioc
+ image_exp_Ioi
+ image_exp_Ioo
+ image_exp_uIcc
+ image_log_Icc
+ image_log_Ici
+ image_log_Ico
+ image_log_Ioc
+ image_log_Ioi
+ image_log_Ioo
+ image_log_uIcc
+ instCoefn
+ integ_div_mul_log_sq
+ integrableOn_Ioi_inv_div_log_sq
+ integrableOn_comp_exp_Ioi
+ integrableOn_comp_log_Ioi
+ integrableOn_log_log_mul_rpow
+ integrable_const_div_mul_log_sq
+ integrable_mul_E₁
+ integral_Ioi_inv_divlog_sq
+ integral_comp_exp_Ioi
+ integral_comp_log_Ioi
+ integral_comp_mul_left_Ioi'
+ integral_comp_mul_right_Ioi'
+ integral_comp_rpow_Ioi_of_pos'
+ integral_inv_div_log
+ integral_inv_div_log_sq
+ inv_div_log_sq_nonneg
+ inv_log_isLittleO_one
+ le_first
+ le_mul_sum_vonMangoldt
+ le_sum_log
+ le_sum_log'
+ le_sum_log_nat
+ le_sum_log_prime_div_sub
+ le_sum_log_prime_div_sub_nat
+ le_sum_vonMangoldt_div_sub
+ le_sum_vonMangoldt_div_sub_nat
+ lo_nonpos
+ log_four_eq
+ log_mul_prod_prime_one_minus_inv_tendsto
+ log_mul_prod_prime_one_minus_inv_tendsto_nat
+ log_riemannZeta_eq
+ log_ten_eq
+ map_one
+ map_zero
+ mul_sum_prime_le
+ neg_inv_sub_log_sub_inv_eq
+ neg_inv_sub_log_sub_inv_le
+ neg_inv_sub_log_sub_inv_nonneg
+ not_continuousAt_log_log_neg_one
+ not_continuousAt_log_log_one
+ not_continuousAt_log_log_zero
+ one_isLittleO_log_log
+ preimage_inv_mul_right_singleton
+ primeFun
+ prod_prime_one_minus_inv_asymp
+ prod_prime_one_minus_inv_asymp_nat
+ prod_prime_one_minus_inv_eq
+ riemannZeta_eq_exp_LSeries
+ sum_asymp
+ sum_asymp_nat
+ sum_div_log_asymp
+ sum_div_log_asymp_nat
+ sum_div_log_eq
+ sum_div_log_eq'
+ sum_div_log_mul_pow_add_tendsto
+ sum_div_log_mul_pow_eq
+ sum_div_log_sub_bounded
+ sum_div_log_sub_bounded_nat
+ sum_div_log_sub_isBigO
+ sum_div_log_sub_isBigO_nat
+ sum_div_log_sub_sub_bound
+ sum_div_log_sub_sub_bound_nat
+ sum_div_log_sub_sub_isBigO
+ sum_div_log_sub_sub_isBigO_nat
+ sum_div_log_sub_sub_isLittleO
+ sum_div_log_sub_sub_isLittleO_nat
+ sum_eq
+ sum_eq'
+ sum_eq_nat
+ sum_log_eq_log_factorial
+ sum_log_eq_sum_mangoldt
+ sum_log_le
+ sum_log_le'
+ sum_log_prime_div_asymp
+ sum_log_prime_div_asymp_nat
+ sum_log_prime_div_sub_bounded
+ sum_log_prime_div_sub_bounded_nat
+ sum_log_prime_div_sub_le
+ sum_prime_div_mul_log_sub_sub_isBigO
+ sum_prime_div_mul_log_sub_sub_isBigO_nat
+ sum_prime_eq
+ sum_prime_inv_asymp
+ sum_prime_inv_asymp_nat
+ sum_prime_inv_sub_isBigO
+ sum_prime_inv_sub_isBigO_nat
+ sum_prime_inv_sub_sub_bound
+ sum_prime_inv_sub_sub_bound_nat
+ sum_prime_inv_sub_sub_isLittleO
+ sum_prime_inv_sub_sub_isLittleO_nat
+ sum_prime_le
+ sum_prime_log_sub_inv_eq
+ sum_prime_log_sub_inv_eq_nat
+ sum_primes_log_sub_add_isBigO
+ sum_primes_log_sub_add_isBigO_nat
+ sum_sub_log_bound
+ sum_sub_log_bound_nat
+ sum_sub_log_bounded
+ sum_sub_log_bounded_nat
+ sum_vonMangoldt_div_asymp
+ sum_vonMangoldt_div_asymp_nat
+ sum_vonMangoldt_div_mul_log_asymp
+ sum_vonMangoldt_div_mul_log_asymp_nat
+ sum_vonMangoldt_div_mul_log_sub_isBigO
+ sum_vonMangoldt_div_mul_log_sub_isBigO_nat
+ sum_vonMangoldt_div_mul_log_sub_sub_bound
+ sum_vonMangoldt_div_mul_log_sub_sub_bound_nat
+ sum_vonMangoldt_div_mul_log_sub_sub_isBigO
+ sum_vonMangoldt_div_mul_log_sub_sub_isBigO_nat
+ sum_vonMangoldt_div_mul_log_sub_sub_isLittleO
+ sum_vonMangoldt_div_mul_log_sub_sub_isLittleO_nat
+ sum_vonMangoldt_div_sub_bounded
+ sum_vonMangoldt_div_sub_bounded_nat
+ sum_vonMangoldt_div_sub_le
+ sum_vonMangoldt_eq
+ sum_vonMangoldt_le_sum_prime_add_E₁
+ tsum_inv_mul_pow_le
+ tsum_primes_eq
+ vonMangoldtFun
++ E₁
++ hasDerivAt_Gamma

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5001	1	exposed public sections

Current commit 363bdfef77
Reference commit e2361c1beb

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Analysis): integral test for infinite sums #40588
• feat(Analysis/Complex/ExponentialBounds): add log 4 and log 10 lemmas #40721
• feat(Analysis/SpecialFunctions/Log/InvLog): add more API for inv_log and log_log #40847
• feat(NumberTheory/EulerProduct/DirichletLSeries): establish Dirichlet series for log of L-functions or Riemann-zeta #41097
• feat(Analysis/SpecialFunctions/Gamma/Deriv,NumberTheory/Harmonic/GammaDeriv): formulae for the derivative of Gamma / eulerMascheroni #41120
• feat(Topology/Algebra/Group/Basic,Algebra/Group/Pointwise/Set/Basic): add Filter.map_{sub,div}{Left,Right}_nhds{,LT,GT,NE} #41376
  By Dependent Issues (🤖). Happy coding!