Prove2Me

Second moment asymptotic ∫0T∣ζ(12+it)∣2dt=T(c1,0log⁡T+c1,1)+o(T)\int_0^T|\zeta(\tfrac12+it)|^{2}dt=T(c_{1,0}\log T+c_{1,1})+o(T) (Littlewood)

Open
LindelofHypothesis.second_moment_asymptotic

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

analytic-number-theorylindelof-hypothesisriemann-zeta

There are real constants c1,0,c1,1c_{1,0},c_{1,1} such that

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

This is the case k=1k=1 of the conjectured asymptotic ∫0T∣ζ(12+it)∣2kdt=T∑j=0k2ck,j(log⁡T)k2−j+o(T)\int_0^T|\zeta(\tfrac12+it)|^{2k}dt=T\sum_{j=0}^{k^2}c_{k,j}(\log T)^{k^2-j}+o(T), proved by Littlewood.

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 second_moment_asymptotic :
    ∃ c : ℕ → ℝ,
      (fun T : ℝ => (∫ t in (0 : ℝ)..T, ‖riemannZeta (1 / 2 + t * I)‖ ^ 2) -
          T * ∑ j ∈ Finset.range 2, c j * Real.log T ^ (1 - 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 = 1 ("This has been proved by Littlewood for k = 1").
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