Hermite's formula at s = 5 for integer arguments

∫₀^∞ w(y) / (y² + j²) dy = j⁴ (ζ(5) - H_j^{(5)}) - 1/4 + 1/(2j) for j ≥ 1, i.e. the pole moments (2.3) of the paper (Proposition 2.2).

theorem Zeta5Irrational.integral_y_div_sq_sq {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, y / (y ^ 2 + a ^ 2) ^ 2 = 1 / (2 * a ^ 2)

∫₀^∞ y/(y² + a²)² dy = 1/(2a²).

theorem Zeta5Irrational.integral_abs_k4_le {a n : ℝ} (ha : 0 < a) (hn : 0 < n) : ∫ (y : ℝ) in Set.Ioi 0, |k4 a n y| ≤ 5 * a / n ^ 2

∫₀^∞ |k4 a n| ≤ 5a / n².

theorem Zeta5Irrational.tsum_tail_eq (j : ℕ) : ∑' (n : ℕ), 1 / (↑j + (↑n + 1)) ^ 5 = zeta5 - ↑(H5 j)

∑_{n ≥ 0} 1/(n + j + 1)⁵ = ζ(5) - H_j^{(5)}.

theorem Zeta5Irrational.hermite_pole (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 (2.3) of the paper).