The polynomial moments of the weight w (first half of Proposition 2.2)

∫₀^∞ y^{2e} w(y) dy = μ(t^e) = (-1)^e B_{2e+2} (2e+3)(2e+4)(2e+5) / 24, from the Gamma integral, term-wise integration of the series defining w, and Euler's formula ζ(2k) = (-1)^{k+1} 2^{2k-1} π^{2k} B_{2k} / (2k)! (hasSum_zeta_nat in Mathlib).

theorem Zeta5Irrational.integral_pow_mul_exp_neg_mul (m : ℕ) {r : ℝ} (hr : 0 < r) : ∫ (y : ℝ) in Set.Ioi 0, y ^ m * Real.exp (-(r * y)) = ↑m.factorial / r ^ (m + 1)

∫₀^∞ y^m e^{-ry} dy = m! / r^(m+1).

theorem Zeta5Irrational.integrableOn_pow_mul_exp_neg_mul (m : ℕ) {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ m * Real.exp (-(r * y))) (Set.Ioi 0) MeasureTheory.volume

noncomputable def Zeta5Irrational.momTerm (e ℓ : ℕ) (y : ℝ) : ℝ

The summand y^{2e} · (2π)⁴ y⁵ / 12 · (ℓ+1)⁴ e^{-2π(ℓ+1)y}.

Equations

• Zeta5Irrational.momTerm e ℓ y = (2 * Real.pi) ^ 4 / 12 * (↑ℓ + 1) ^ 4 * (y ^ (2 * e + 5) * Real.exp (-(2 * Real.pi * (↑ℓ + 1) * y)))

theorem Zeta5Irrational.momTerm_eq (e ℓ : ℕ) (y : ℝ) : momTerm e ℓ y = y ^ (2 * e) * ((2 * Real.pi) ^ 4 * y ^ 5 / 12) * ((↑ℓ + 1) ^ 4 * Real.exp (-(2 * Real.pi * (↑ℓ + 1) * y)))

theorem Zeta5Irrational.integrableOn_momTerm (e ℓ : ℕ) : MeasureTheory.IntegrableOn (momTerm e ℓ) (Set.Ioi 0) MeasureTheory.volume

theorem Zeta5Irrational.integral_momTerm (e ℓ : ℕ) : ∫ (y : ℝ) in Set.Ioi 0, momTerm e ℓ y = (2 * Real.pi) ^ 4 / 12 * ↑(2 * e + 5).factorial / (2 * Real.pi) ^ (2 * e + 6) * (1 / (↑ℓ + 1) ^ (2 * e + 2))

theorem Zeta5Irrational.momTerm_nonneg (e ℓ : ℕ) {y : ℝ} (hy : 0 < y) : 0 ≤ momTerm e ℓ y

theorem Zeta5Irrational.mono_moment (e : ℕ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ (2 * e) * w y) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Ioi 0, y ^ (2 * e) * w y = ↑(μmono e)

The polynomial moments: ∫₀^∞ y^{2e} w(y) dy = μ(t^e), with integrability.