Prove2Me

Ingham's zero-density estimate N(σ,T)≪T32−σ(1−σ)+εN(\sigma,T)\ll T^{\frac{3}{2-\sigma}(1-\sigma)+\varepsilon}

Proved
LindelofHypothesis.ingham_density_estimate

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

analytic-number-theorylindelof-hypothesisriemann-zeta

Let N(σ,T)N(\sigma,T) be the number of zeros ρ\rho of ζ\zeta with Re⁡ρ≥σ\operatorname{Re}\rho\ge\sigma and ∣Im⁡ρ∣≤T|\operatorname{Im}\rho|\le T, counted with multiplicity. For every σ∈[12,1]\sigma\in[\tfrac12,1] and every ε>0\varepsilon>0,

N(σ,T)≪TAI(σ)(1−σ)+ε,AI(σ)=32−σ.N(\sigma,T)\ll T^{A_I(\sigma)(1-\sigma)+\varepsilon},\qquad A_I(\sigma)=\frac{3}{2-\sigma}.

This is Ingham's 1940 zero-density estimate, unconditional.

Formalization Note Stated in the form N(σ,T)≪TA(σ)(1−σ)+εN(\sigma,T)\ll T^{A(\sigma)(1-\sigma)+\varepsilon} of the source, on the range 12≤σ≤1\tfrac12\le\sigma\le1 of Ingham's theorem. 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 ingham_density_estimate (σ : ℝ) (hσ₀ : 1 / 2 ≤ σ) (hσ₁ : σ ≤ 1) (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, ∀ᶠ T in atTop,
      (zeroDensityCount σ T : ℝ≥0∞) ≤ ENNReal.ofReal (C * T ^ (3 / (2 - σ) * (1 - σ) + ε)) := 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 "The density hypothesis", sentence "Ingham showed that A_I(σ) = 3/(2 − σ) in 1940".
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).

  • Endorsed by dbenbenn · Nov 6, 2026

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

View graph