Zeros with $T\le\operatorname{Im}\rho\le T+1$ : $O(\log T)$

Proved

LindelofHypothesis.zeroCountWindowAll_isBigO_log

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

analytic-number-theorylindelof-hypothesisriemann-zeta

The number of zeros $\rho$ of $\zeta$ with $T\le\operatorname{Im}\rho\le T+1$ , counted with multiplicity, is $O(\log T)$ as $T\to\infty$ : there is a constant $C$ such that for all sufficiently large $T$ ,

\#\{\rho:\ \zeta(\rho)=0,\ T\le\operatorname{Im}\rho\le T+1\}\le C\log T .

The source contrasts this known bound with Backlund's reformulation of the Lindelöf hypothesis, which asks for $o(\log T)$ zeros to the right of $\operatorname{Re}s=\tfrac12+\varepsilon$ .

Formalization Note Counts are elements of $\mathbb N\cup\{\infty\}$ (cast to $[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 zeroCountWindowAll_isBigO_log :
    ∃ C : ℝ, ∀ᶠ T in atTop, (zeroCountWindowAll 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", sentence "The number of zeros with imaginary part between T and T + 1 is known to be O(log(T))".

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

Zeros with T≤Im⁡ρ≤T+1T\le\operatorname{Im}\rho\le T+1T≤Imρ≤T+1: O(log⁡T)O(\log T)O(logT)

Zeros with $T\le\operatorname{Im}\rho\le T+1$ : $O(\log T)$