RiemannZetaMoments.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 6 contain sorry, 0 declared as axioms

Moments of the Riemann zeta function on the critical line

The moments $\frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}\,dt$ are conjectured to be asymptotic to $c_k (\log T)^{k^2}$ for some constants $c_k$. This is a theorem for $k = 1$ (Hardy–Littlewood, $c_1 = 1$) and $k = 2$ (Ingham, $c_2 = 1/(2\pi^2)$), and these are the only proven cases. Conrey–Ghosh and Conrey–Gonek conjectured $c_3 = 42 a_3 / 9!$ and $c_4 = 24024 a_4 / 16!$, with $a_k$ the arithmetic factor $a_k = \prod_p (1 - 1/p)^{k^2} \sum_{m \ge 0} \binom{m+k-1}{m}^2 p^{-m}$; Keating–Snaith conjectured $c_k = a_k f_k$ with $f_k = \prod_{j=0}^{k-1} j!/(j+k)!$ from random matrix theory, recovering $g_k = (k^2)!\,f_k = 1, 2, 42, 24024$.

The statements and constants below are taken from §3.4.5 of [Co26].

References:

[Co26] A. Connes, The Riemann Hypothesis: Past, Present and a Letter Through Time, arXiv:2602.04022, §3.4.5.
[In26] A. E. Ingham, Mean-value theorems in the theory of the Riemann zeta-function, Proc. London Math. Soc. 27 (1926), 273–300.
[CG98] J. B. Conrey, A. Ghosh, A conjecture for the sixth power moment of the Riemann zeta-function, Internat. Math. Res. Notices 1998, no. 15, 775–780.
[CGo01] J. B. Conrey, S. Gonek, High moments of the Riemann zeta-function, Duke Math. J. 107 (2001), no. 3, 577–604.
[KS00] J. P. Keating, N. C. Snaith, Random matrix theory and $\zeta(1/2+it)$, Commun. Math. Phys. 214 (2000), no. 1, 57–89.

Imports (1)

FormalConjecturesUtil

def RiemannZetaMoments.moment The $k$th moment of the Riemann zeta function is the integral $$ \frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}dt. $$ line 59 source
Source documentation
The $k$th moment of the Riemann zeta function is the integral $$ \frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}dt. $$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HMul.hMul, HDiv.hDiv, OfNat.ofNat, intervalIntegral, HPow.hPow, Norm.norm, Complex, riemannZeta, HAdd.hAdd, Complex.I, MeasureTheory.MeasureSpace.volume
31 instances, coercions and auxiliary constants left out.
```
noncomputable def moment (k : ℕ) (T : ℝ) : ℝ :=
…
```
theorem RiemannZetaMoments.moment_isEquiv Documented declaration: moment_isEquiv sorry line 70 source
Source documentation
The asymptotic behaviour of the $k$th moment of the Riemann zeta function is conjectured to be $$ \frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}dt \sim c_k \log(T)^{k^2}, $$ for some constant $c_k$.

depends on sorry what this means
Statement uses: Nat, Exists, Real, And, GT.gt, OfNat.ofNat, Asymptotics.IsEquivalent, Filter.atTop, RiemannZetaMoments.moment, HMul.hMul, HPow.hPow, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem moment_isEquiv (k : ℕ) : ∃ c > (0 : ℝ),
    moment k ~[atTop] fun T ↦ c * T.log ^ (k ^ 2) := by
…
```
Mentions: c, RiemannZetaMoments.moment
theorem RiemannZetaMoments.moment_isEquiv₁ The asymptotic behaviour of the first moment of the Riemann zeta function was proved by Hardy and Littlewood, where $c_1 = 1$ [Co26, §3.4.5] sorry line 77 source
Source documentation
The asymptotic behaviour of the first moment of the Riemann zeta function was proved by Hardy and Littlewood, where $c_1 = 1$ [Co26, §3.4.5].

depends on sorry what this means
Statement uses: Asymptotics.IsEquivalent, Real, Filter.atTop, RiemannZetaMoments.moment, OfNat.ofNat, Nat, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem moment_isEquiv₁ : moment 1 ~[atTop] fun T ↦ T.log := by
…
```
Mentions: RiemannZetaMoments.moment
theorem RiemannZetaMoments.moment_isEquiv₂ The asymptotic behaviour of the second moment of the Riemann zeta function was proved by Ingham [In26], where $c_2 = 1/(2\pi^2)$ sorry line 83 source
Source documentation
The asymptotic behaviour of the second moment of the Riemann zeta function was proved by Ingham [In26], where $c_2 = 1/(2\pi^2)$.

depends on sorry what this means
Statement uses: Asymptotics.IsEquivalent, Real, Filter.atTop, RiemannZetaMoments.moment, OfNat.ofNat, Nat, HMul.hMul, HDiv.hDiv, HPow.hPow, Real.pi, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem moment_isEquiv₂ : moment 2 ~[atTop] fun T ↦ (1 / (2 * π ^ 2)) * T.log ^ 4 := by
…
```
Mentions: RiemannZetaMoments.moment
def RiemannZetaMoments.arithmeticFactor Documented declaration: arithmeticFactor line 94 source
Source documentation
The arithmetic factor expected to appear in the asymptotic behaviour of the $k$th moment of the Riemann zeta function, defined by $$ a_k = \prod_{p \text{ prime}} (1 - 1/p)^{k^2} \sum_{m=0}^{\infty} \binom{m+k-1}{m}^2 p^{-m}. $$ For $k \ge 1$ we have $\binom{m+k-1}{m} = \Gamma(m+k)/(m!\,\Gamma(k))$. We use Nat.multichoose, so that $a_0 = 1$ and the Keating–Snaith formula also holds for $k = 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: tprod, Nat.Primes, HMul.hMul, HPow.hPow, HSub.hSub, OfNat.ofNat, HDiv.hDiv, Nat.Prime, tsum, Nat.multichoose, SummationFilter.unconditional
23 instances, coercions and auxiliary constants left out.
```
noncomputable def arithmeticFactor (k : ℕ) : ℝ :=
…
```
theorem RiemannZetaMoments.arithmeticFactor_zero line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, RiemannZetaMoments.arithmeticFactor, OfNat.ofNat, Nat
Proof uses: Nat.Primes, tsum, HDiv.hDiv, HPow.hPow, Nat.multichoose, Nat.Prime, SummationFilter.unconditional, Eq.mpr, id, congrArg, tsum_eq_single, Ne, Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, of_eq_true, Eq.trans, True, congrFun', HAdd.hAdd and 25 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem RiemannZetaMoments.moment_isEquiv₃ The constant in the asymptotic formula for the 3rd zeta moment is conjectured to be $42a_3/9!$ [CG98] sorry line 109 source
Source documentation
The constant in the asymptotic formula for the 3rd zeta moment is conjectured to be $42a_3/9!$ [CG98].

depends on sorry what this means
Statement uses: Asymptotics.IsEquivalent, Real, Filter.atTop, RiemannZetaMoments.moment, OfNat.ofNat, Nat, HMul.hMul, HDiv.hDiv, RiemannZetaMoments.arithmeticFactor, Nat.factorial, HPow.hPow, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem moment_isEquiv₃ : moment 3 ~[atTop] fun T ↦ 42 * arithmeticFactor 3 / 9 ! * T.log ^ 9 := by
…
```
Mentions: RiemannZetaMoments.moment, RiemannZetaMoments.arithmeticFactor
theorem RiemannZetaMoments.moment_isEquiv₄ The constant in the asymptotic formula for the 4th zeta moment is conjectured to be $24024a_4/16!$ [CGo01] sorry line 115 source
Source documentation
The constant in the asymptotic formula for the 4th zeta moment is conjectured to be $24024a_4/16!$ [CGo01].

depends on sorry what this means
Statement uses: Asymptotics.IsEquivalent, Real, Filter.atTop, RiemannZetaMoments.moment, OfNat.ofNat, Nat, HMul.hMul, HDiv.hDiv, RiemannZetaMoments.arithmeticFactor, Nat.factorial, HPow.hPow, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem moment_isEquiv₄ :
    moment 4 ~[atTop] fun T ↦ 24024 * arithmeticFactor 4 / 16 ! * T.log ^ 16 := by
…
```
Mentions: RiemannZetaMoments.moment, RiemannZetaMoments.arithmeticFactor
theorem RiemannZetaMoments.moment_isEquivₖ The Keating–Snaith conjecture [KS00] for the $k$th moment of the Riemann zeta function, provides the value of $c_k$ in the asymptotic formula [Co26, §3.4.5] sorry line 122 source
Source documentation
The Keating–Snaith conjecture [KS00] for the $k$th moment of the Riemann zeta function, provides the value of $c_k$ in the asymptotic formula [Co26, §3.4.5].

depends on sorry what this means
Statement uses: Nat, Asymptotics.IsEquivalent, Real, Filter.atTop, RiemannZetaMoments.moment, HMul.hMul, RiemannZetaMoments.arithmeticFactor, Finset.prod, Finset.range, HDiv.hDiv, Nat.factorial, HAdd.hAdd, HPow.hPow, Real.log, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem moment_isEquivₖ (k : ℕ) : moment k ~[atTop]
    fun T ↦ (arithmeticFactor k * ∏ j ∈ Finset.range k, (j ! : ℝ) / (j + k) !) *
      T.log ^ (k ^ 2) := by
…
```
Mentions: RiemannZetaMoments.moment, RiemannZetaMoments.arithmeticFactor