Prove2Me

Fourth moment asymptotic ∫0T∣ζ(12+it)∣4dt=T∑j=04c2,j(log⁡T)4−j+o(T)\int_0^T|\zeta(\tfrac12+it)|^{4}dt=T\sum_{j=0}^{4}c_{2,j}(\log T)^{4-j}+o(T) (Heath-Brown)

Open
LindelofHypothesis.fourth_moment_asymptotic

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

analytic-number-theorylindelof-hypothesisriemann-zeta

There are real constants c2,0,…,c2,4c_{2,0},\dots,c_{2,4} such that

∫0T∣ζ ⁣(12+it)∣4dt=T∑j=04c2,j (log⁡T)4−j+o(T)(T→∞).\int_0^T\left|\zeta\!\left(\tfrac12+it\right)\right|^{4}dt=T\sum_{j=0}^{4}c_{2,j}\,(\log T)^{4-j}+o(T)\qquad(T\to\infty).

This is the case k=2k=2 of the conjectured moment asymptotic, proved by Heath-Brown (extending Ingham, who found the leading term).

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 fourth_moment_asymptotic :
    ∃ c : ℕ → ℝ,
      (fun T : ℝ => (∫ t in (0 : ℝ)..T, ‖riemannZeta (1 / 2 + t * I)‖ ^ 4) -
          T * ∑ j ∈ Finset.range 5, c j * Real.log T ^ (4 - j))
        =o[atTop] (fun T : ℝ => 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 "Means of powers (or moments) of the zeta function", second displayed formula with k = 2 ("and by Heath-Brown for k = 2 (extending a result of Ingham who found the leading term)").
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