The Riemann hypothesis implies the Lindelöf hypothesis

Open

LindelofHypothesis.lindelof_of_riemannHypothesis

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

analytic-number-theorylindelof-hypothesisriemann-zeta

Assume the Riemann hypothesis: every zero $s$ of $\zeta$ other than the trivial zeros $-2,-4,-6,\dots$ has $\operatorname{Re}s=\tfrac12$ . Then the Lindelöf hypothesis holds: for every $\varepsilon>0$ ,

\zeta\!\left(\tfrac12+it\right)=O\!\left(t^{\varepsilon}\right)\qquad(t\to+\infty).

Formalization Note The Riemann hypothesis is Mathlib's RiemannHypothesis. RiemannVonMangoldt.LindelofHypothesis is the published definition: for every $\varepsilon>0$ , $\zeta(\tfrac12+it)=O(t^{\varepsilon})$ as $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_of_riemannHypothesis (hRH : RiemannHypothesis) : RiemannVonMangoldt.LindelofHypothesis := 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 ("This hypothesis is implied by the Riemann hypothesis") and section "Relation to the Riemann hypothesis".

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