The Hankel determinant as a multiple integral, (6.10)

Δ_K(ζ(5)) = (1/h!) ∫_{(0,∞)^h} det(V(y))² ∏ᵢ ν(yᵢ) dy, where V(y) is the Vandermonde matrix of y₁², …, y_h² and ν(y) = D_N(y²)^6 / D_K(y²) · w(y).

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.μpos : MeasureTheory.Measure ℝ

The measure dy on (0, ∞).

Equations

• Zeta5Irrational.μpos = MeasureTheory.volume.restrict (Set.Ioi 0)

theorem Zeta5Irrational.Δ_eq_integral (n : ℕ) : (Polynomial.aeval zeta5) (Δ n) = 1 / ↑(37 * n).factorial * ∫ (x : Fin (37 * n) → ℝ), (Matrix.vandermonde fun (j : Fin (37 * n)) => x j ^ 2).det ^ 2 * ∏ j : Fin (37 * n), ν n (x j) ∂MeasureTheory.Measure.pi fun (x : Fin (37 * n)) => μpos

(6.10): the Hankel determinant as a multiple integral.