Harmonic upper comparison (Lagarias Lemma 3.2)

Proved

LeanEval.NumberTheory.lagarias_harmonic_upper_bound

by xuanji · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

lagariasnumber-theoryriemann-hypothesis

Let $\gamma$ be Euler's constant. For every natural number $n\ge20$ ,

H_n+\exp(H_n)\log(H_n)\le e^\gamma n\log\log n+\frac{7n}{\log n}.

This unconditional upper estimate retains both the source's numerical constant and its threshold; neither is an assumed asymptotic placeholder.

Preamble

import Mathlib.NumberTheory.ArithmeticFunction.Misc
import Mathlib.NumberTheory.Harmonic.Defs
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.Harmonic.EulerMascheroni

open scoped ArithmeticFunction.sigma

Formal statement

namespace LeanEval.NumberTheory

theorem lagarias_harmonic_upper_bound (n : ℕ) (hn : 20 ≤ n) :
    (harmonic n : ℝ) +
      Real.exp (harmonic n : ℝ) * Real.log (harmonic n : ℝ) ≤
      Real.exp Real.eulerMascheroniConstant * (n : ℝ) * Real.log (Real.log (n : ℝ)) +
        7 * (n : ℝ) / Real.log (n : ℝ) := by sorry

end LeanEval.NumberTheory

Source

Jeffrey C. Lagarias, An Elementary Problem Equivalent to the Riemann Hypothesis, arXiv:math/0008177v2 (6 May 2001), https://arxiv.org/abs/math/0008177v2, p. 7, Lemma 3.2, equation (3.7).

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

For every natural number $n$ with $n\ge 20$ , let $H_n=\sum_{k=1}^{n}1/k$ , regarded as a real number, and let $\gamma=\lim_{m\to\infty}(H_m-\log(m+1))$ be the Euler–Mascheroni constant. Then $H_n+e^{H_n}\log H_n\le e^\gamma n\log(\log n)+7n/\log n$ , where $\log$ denotes the natural logarithm. The hypothesis excludes $n=0$ and ensures that all logarithm arguments and the denominator $\log n$ in this inequality are positive.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by xuanji · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph