Robin oscillation under failure of RH (Lagarias Proposition 3.2)

Open

LeanEval.NumberTheory.lagarias_robin_oscillation

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

lagariasnumber-theoryriemann-hypothesis

Assume that the Riemann hypothesis is false. There exist fixed real constants $\beta,C$ with $0<\beta<1/2$ and $C>0$ such that arbitrarily large integers $n\ge3$ satisfy

\sigma(n)\ge e^\gamma n\log\log n+\frac{Cn\log\log n}{(\log n)^\beta}.

The same constants work for all cutoffs: for every natural number $N$ , such an $n\ge N$ exists. This is the infinite-set statement of Proposition 3.2 with the finitely many indices below 3 removed, so the denominator uses a positive logarithm and an actual real power. It is a substantial oscillation theorem, not merely the assertion that Robin's inequality has a counterexample.

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_oscillation (hRH : ¬ RiemannHypothesis) :
    ∃ β C : ℝ, 0 < β ∧ β < 1 / 2 ∧ 0 < C ∧
      ∀ N : ℕ, ∃ n : ℕ, N ≤ n ∧ 3 ≤ n ∧
        Real.exp Real.eulerMascheroniConstant * (n : ℝ) * Real.log (Real.log (n : ℝ)) +
            C * (n : ℝ) * Real.log (Real.log (n : ℝ)) /
              Real.rpow (Real.log (n : ℝ)) β ≤
          ((σ 1 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.2, equation (3.2); attributed there to Robin (1984), §4, Proposition 1. Infinite set of indices expressed as unboundedness in ℕ, with finitely many n < 3 excluded.

Read-back

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

Assume the Riemann hypothesis is false, meaning that there exists $s\in\mathbb C$ with $\zeta(s)=0$ , with $s\ne-2(k+1)$ for every natural number $k$ , with $s\ne1$ , and with $\operatorname{Re}(s)\ne\tfrac12$ , where $\zeta$ is the Riemann zeta function. Then there exist real constants $\beta$ and $C$ satisfying $0<\beta<\tfrac12$ and $C>0$ such that, for every natural number $N$ (including $0$ ), there exists a natural number $n$ with $N\le n$ and $n\ge3$ for which $e^\gamma n\log(\log n)+\dfrac{Cn\log(\log n)}{(\log n)^\beta}\le\sum_{d\mid n,\ d>0}d$ . Here $\gamma=\lim_{m\to\infty}\left(\sum_{j=1}^{m}\frac1j-\log(m+1)\right)$ is the Euler–Mascheroni constant, the sum on the right is over the positive natural-number divisors of $n$ , and the power in the denominator is a real power. The restriction $n\ge3$ ensures that the logarithms have positive arguments and the denominator is nonzero.

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