Prove2Me

Backlund: Lindelöf   ⟺  \iffo(log⁡T)o(\log T) zeros with Re⁡ρ≥12+ε\operatorname{Re}\rho\ge\tfrac12+\varepsilon, T≤Im⁡ρ≤T+1T\le\operatorname{Im}\rho\le T+1

Open
LindelofHypothesis.backlund_lindelof_iff

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

analytic-number-theorylindelof-hypothesisriemann-zeta

The Lindelöf hypothesis holds if and only if, for every ε>0\varepsilon>0, the number of zeros ρ\rho of ζ\zeta with

Re⁡ρ≥12+ε,T≤Im⁡ρ≤T+1,\operatorname{Re}\rho\ge\tfrac12+\varepsilon,\qquad T\le\operatorname{Im}\rho\le T+1,

counted with multiplicity, is o(log⁡T)o(\log T) as T→∞T\to\infty.

This is Backlund's (1918–1919) reformulation of the Lindelöf hypothesis as a statement about zeros; it shows why the Riemann hypothesis implies it.

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. o(log⁡T)o(\log T) is written out: for every c>0c>0 the count is eventually at most clog⁡Tc\log T. Counts are elements of N∪{∞}\mathbb N\cup\{\infty\} (cast to [0,∞][0,\infty]), so the bound also asserts that the count is finite.

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 backlund_lindelof_iff :
    RiemannVonMangoldt.LindelofHypothesis ↔
      ∀ ε : ℝ, 0 < ε → ∀ c : ℝ, 0 < c →
        ∀ᶠ T in atTop, (zeroCountWindow (1 / 2 + ε) T : ℝ≥0∞) ≤ ENNReal.ofReal (c * Real.log 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; section "Relation to the Riemann hypothesis", first sentence (Backlund 1918–1919).
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