Robin conditional upper bound (Lagarias Proposition 3.1)

Open

LeanEval.NumberTheory.lagarias_robin_upper_bound

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

lagariasnumber-theoryriemann-hypothesis

Assume the Riemann hypothesis. For every natural number $n\ge5041$ ,

\sigma(n)\le e^\gamma n\log\log n.

Here $\gamma$ is Euler's constant. This is the non-strict formulation in Lagarias's Proposition 3.1, attributed there to Robin's Theorem 1. It is a major conditional analytic theorem to formalize, not an assumption made available for free and not a request to prove RH.

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_robin_upper_bound (hRH : RiemannHypothesis) (n : ℕ) (hn : 5041 ≤ n) :
    ((σ 1 n : ℕ) : ℝ) ≤
      Real.exp Real.eulerMascheroniConstant * (n : ℝ) * Real.log (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. 6, Proposition 3.1, equation (3.1); attributed there to Robin (1984), Theorem 1.

Read-back

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

Assume the Riemann hypothesis in the following precise form: every $s\in\mathbb C$ satisfying $\zeta(s)=0$ , $s\ne-2(k+1)$ for every natural number $k\ge0$ , and $s\ne1$ has real part $1/2$ , where $\zeta$ is the Riemann zeta function. Then, for every natural number $n$ with $n\ge5041$ , the sum of its positive divisors, regarded as a real number, satisfies $\sum_{d\mid n,\ d>0}d\le e^\gamma n\log(\log n)$ , where $\gamma=\lim_{m\to\infty}\left(\sum_{j=1}^{m}\frac1j-\log(m+1)\right)$ is the Euler–Mascheroni constant and $\log$ denotes the natural logarithm. The lower bound on $n$ excludes $n=0$ and ensures both logarithms have positive arguments.

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