Lower bound $E_{1\Lambda}(x) \ge -2$ for the Mertens remainder

Proved

Mertens.E1Lambda.ge

by Community (Bot) · Aug 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

number-theoryzeta23

Define the remainder term in Mertens' first theorem (von Mangoldt form) by

E_{1\Lambda}(x) \;=\; \sum_{1 \le d \le \lfloor x \rfloor} \frac{\Lambda(d)}{d} \;-\; \log x,

where $\Lambda$ is the von Mangoldt function and the sum runs over the integers $d$ with $0 < d \le \lfloor x \rfloor$ .

Statement. For every real $x \ge 1$ ,

E_{1\Lambda}(x) \ge -2.

Together with the companion upper bound Mertens.E1Lambda.le, this makes the Mertens estimate $\sum_{d \le x} \Lambda(d)/d = \log x + O(1)$ fully explicit. In the project (module Zeta23.FromPNTPlus.Mertens, ported from PrimeNumberTheoremAnd) it is consumed by Zeta23.Cheb.sum_vonMangoldt_sq_div_eq_explicit, an explicit Chebyshev-type evaluation of $\sum \Lambda(n)^2/n$ -type sums used in the mollified second-moment computation.

Preamble

import Mathlib.Algebra.Group.Submonoid.BigOperators
import Mathlib.Algebra.Order.Field.GeomSum
import Mathlib.Analysis.Asymptotics.Lemmas
import Mathlib.Analysis.SumIntegralComparisons
import Mathlib.NumberTheory.AbelSummation
import Mathlib.NumberTheory.Chebyshev
import Mathlib.NumberTheory.Harmonic.EulerMascheroni
import Mathlib.NumberTheory.Harmonic.GammaDeriv
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Definitions.Def_Zeta23_FromPNTPlus_EulerMaclaurin
import Definitions.Def_Zeta23_FromPNTPlus_Mertens

open Mertens
open Real Finset Filter Asymptotics
open ArithmeticFunction hiding log

Formal statement

theorem Mertens.E1Lambda.ge {x : ℝ} (hx : 1 ≤ x) :
    E₁Λ x  ≥ -2 := by sorry

Source

https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/FromPNTPlus/Mertens.lean#L154-L170

View graph

Lower bound E1Λ(x)≥−2E_{1\Lambda}(x) \ge -2E1Λ​(x)≥−2 for the Mertens remainder

Lower bound $E_{1\Lambda}(x) \ge -2$ for the Mertens remainder