Harmonic lower comparison (Lagarias Lemma 3.1)

Proved

LeanEval.NumberTheory.lagarias_harmonic_lower_bound

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

lagariasnumber-theoryriemann-hypothesis

Let $\gamma$ be Euler's constant and $H_n$ the $n$ th harmonic number. For every natural number $n\ge3$ ,

e^\gamma n\log\log n\le \exp(H_n)\log(H_n).

This is an unconditional lower comparison between the elementary harmonic expression and the classical divisor-sum scale.

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_lower_bound (n : ℕ) (hn : 3 ≤ n) :
    Real.exp Real.eulerMascheroniConstant * (n : ℝ) * Real.log (Real.log (n : ℝ)) ≤
      Real.exp (harmonic n : ℝ) * Real.log (harmonic 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, pp. 6–7, Lemma 3.1, equation (3.3).

Read-back

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

For every natural number $n$ with $n\ge 3$ , let $H_n=\sum_{k=1}^{n}1/k$ , viewed as a real number, and let $\gamma=\lim_{m\to\infty}(H_m-\log(m+1))$ be the real Euler–Mascheroni constant. Then $e^\gamma n\log(\log n)\le e^{H_n}\log H_n$ , where $\log$ is the natural logarithm. The hypothesis excludes $n=0,1,2$ and ensures that all logarithm arguments 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