Prove2Me

Lindelöf hypothesis: big-OO and little-oo forms are equivalent

Proved
LindelofHypothesis.lindelof_iff_isLittleO

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorylindelof-hypothesisriemann-zeta

The Lindelöf hypothesis — for every ε>0\varepsilon>0,

ζ ⁣(12+it)=O ⁣(tε)(t→+∞)\zeta\!\left(\tfrac12+it\right)=O\!\left(t^{\varepsilon}\right)\qquad(t\to+\infty)

— is equivalent to the statement that for every ε>0\varepsilon>0,

ζ ⁣(12+it)=o ⁣(tε)(t→+∞).\zeta\!\left(\tfrac12+it\right)=o\!\left(t^{\varepsilon}\right)\qquad(t\to+\infty).

This is the restatement in the opening paragraph of the source ("since ε\varepsilon can be replaced by a smaller value").

Formalization Note RiemannVonMangoldt.LindelofHypothesis is the published definition: for every ε>0\varepsilon>0, ζ(12+it)=O(tε)\zeta(\tfrac12+it)=O(t^{\varepsilon}) as t→+∞t\to+\infty.

Preamble
import Mathlib
import Definitions.Def_RiemannVonMangoldt_ZeroCounts
import Definitions.Def_LindelofHypothesis_GrowthAndZeroCounts

open Complex Filter Asymptotics
open scoped ENNReal
Formal statement
namespace LindelofHypothesis

theorem lindelof_iff_isLittleO :
    RiemannVonMangoldt.LindelofHypothesis ↔
      ∀ ε : ℝ, 0 < ε →
        (fun t : ℝ => riemannZeta (1 / 2 + t * I)) =o[atTop] (fun t : ℝ => t ^ ε) := by sorry

end LindelofHypothesis
Source
Wikipedia, "Lindelöf hypothesis" (snapshot supplied as Lindelöf_hypothesis.pdf, printed 12 Oct 2026), https://en.wikipedia.org/wiki/Lindel%C3%B6f_hypothesis; lead section, displayed formulas 1 and 2.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph