Proposition 2.2: the moment representation, and positivity of Δ_K(ζ(5))

• pole_moment : Hermite's formula at s = 5, ∫₀^∞ w(y) / (y² + j²) dy = j⁴ (ζ(5) - H_j^{(5)}) - 1/4 + 1/(2j) — proved in Zeta5Irrational.HermiteFormula (four integrations by parts and the Mittag-Leffler expansion);
• moment_rep : μ_{ζ(5)}(P / D_K) = ∫₀^∞ (P / D_K)(y²) w(y) dy with integrability, proved from the polynomial moments (mono_moment), the pole moments and the partial fractions (Proposition 2.2 is now fully proved);
• Δ_pos : Δ_K(ζ(5)) > 0, since G_K(ζ(5)) is the Gram matrix of a positive weight.

theorem Zeta5Irrational.pole_moment (j : ℕ) (hj : 1 ≤ j) : ∫ (y : ℝ) in Set.Ioi 0, w y / (y ^ 2 + ↑j ^ 2) = ↑j ^ 4 * (zeta5 - ↑(H5 j)) - 1 / 4 + 1 / (2 * ↑j)

Hermite's formula at s = 5 (the pole moments of Proposition 2.2), proved in Zeta5Irrational.HermiteFormula.

theorem Zeta5Irrational.integrableOn_pole (j : ℕ) (hj : 1 ≤ j) : MeasureTheory.IntegrableOn (fun (y : ℝ) => w y / (y ^ 2 + ↑j ^ 2)) (Set.Ioi 0) MeasureTheory.volume

noncomputable def Zeta5Irrational.integrand (K : ℕ) (P : Polynomial ℚ) (y : ℝ) : ℝ

P(y²) / D_K(y²) · w(y).

Equations

• Zeta5Irrational.integrand K P y = (Polynomial.aeval (y ^ 2)) P / (Polynomial.aeval (y ^ 2)) (Zeta5Irrational.D K) * Zeta5Irrational.w y

theorem Zeta5Irrational.integrand_eq_sum (K : ℕ) (P : Polynomial ℚ) {y : ℝ} (hy : 0 < y) : integrand K P y = ∑ e ∈ Finset.range ((P /ₘ D K).natDegree + 1), ↑((P /ₘ D K).coeff e) * (y ^ (2 * e) * w y) + ∑ j ∈ Finset.Icc 1 K, ↑(res K P j) * (w y / (y ^ 2 + ↑j ^ 2))

The pointwise decomposition of the integrand, for y > 0.

theorem Zeta5Irrational.aeval_μX (K : ℕ) (P : Polynomial ℚ) : (Polynomial.aeval zeta5) (μX K P) = ∑ e ∈ Finset.range ((P /ₘ D K).natDegree + 1), ↑((P /ₘ D K).coeff e) * ↑(μmono e) + ∑ j ∈ Finset.Icc 1 K, ↑(res K P j) * (↑j ^ 4 * (zeta5 - ↑(H5 j)) - 1 / 4 + 1 / (2 * ↑j))

The value μ_{ζ(5)}(P / D_K) in terms of the coefficients of the quotient and residues.

theorem Zeta5Irrational.moment_rep (K : ℕ) (P : Polynomial ℚ) : MeasureTheory.IntegrableOn (integrand K P) (Set.Ioi 0) MeasureTheory.volume ∧ (Polynomial.aeval zeta5) (μX K P) = ∫ (y : ℝ) in Set.Ioi 0, integrand K P y

Proposition 2.2 (the moment representation): for every polynomial P, the function (P / D_K)(y²) w(y) is integrable on (0, ∞) and its integral is μ_{ζ(5)}(P / D_K).

noncomputable def Zeta5Irrational.ν (n : ℕ) (y : ℝ) : ℝ

The positive weight ν(y) = D_N(y²)^6 / D_K(y²) · w(y).

Equations

• Zeta5Irrational.ν n y = (Polynomial.aeval (y ^ 2)) (Zeta5Irrational.D (3 * n)) ^ 6 / (Polynomial.aeval (y ^ 2)) (Zeta5Irrational.D (40 * n)) * Zeta5Irrational.w y

theorem Zeta5Irrational.ν_pos (n : ℕ) {y : ℝ} (hy : 0 < y) : 0 < ν n y

theorem Zeta5Irrational.integrand_eq (n i j : ℕ) (y : ℝ) : integrand (40 * n) (D (3 * n) ^ 6 * Polynomial.X ^ (i + j)) y = (y ^ 2) ^ i * (y ^ 2) ^ j * ν n y

theorem Zeta5Irrational.Δ_pos (n : ℕ) (_hn : 0 < n) : 0 < (Polynomial.aeval zeta5) (Δ n)

Positivity: Δ_K(ζ(5)) > 0, from the moment representation.