Prove2Me

Ingham: under Lindelöf, gn≪pn1/2+εg_n\ll p_n^{1/2+\varepsilon}

Open
LindelofHypothesis.ingham_primeGap_of_lindelof

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

analytic-number-theorylindelof-hypothesisriemann-zeta

Let pnp_n be the nn-th prime and gn=pn+1−png_n=p_{n+1}-p_n. Assume the Lindelöf hypothesis. Then for every ε>0\varepsilon>0,

gn≪pn1/2+εg_n\ll p_n^{1/2+\varepsilon}

for all sufficiently large nn, i.e. gn=O(pn1/2+ε)g_n=O(p_n^{1/2+\varepsilon}) as n→∞n\to\infty.

This is Ingham's consequence of the Lindelöf hypothesis for gaps between consecutive primes.

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. Primes are indexed from 00 (p0=2p_0=2), which does not affect the asymptotic statement.

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_primeGap_of_lindelof (hL : RiemannVonMangoldt.LindelofHypothesis)
    (ε : ℝ) (hε : 0 < ε) :
    (fun n : ℕ => (primeGap n : ℝ)) =O[atTop] (fun n : ℕ => (Nat.nth Nat.Prime n : ℝ) ^ (1 / 2 + ε)) := 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 "Other consequences", first displayed formula (result of Albert Ingham).
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