Towards Hermite's formula at s = 5: the calculus ingredients

• the closed form ∑_{ℓ ≥ 1} ℓ⁴ x^ℓ = x (1 + 11x + 11x² + x³) / (1 - x)⁵ for 0 ≤ x < 1;
• F(y) = 1 / (e^{2πy} - 1) and its derivatives F₁, …, F₄ (explicit rational functions of q = e^{2πy}), with w(y) = y⁵ F₄(y) / 12;
• g(y) = y⁵ / (12 (y² + a²)) and its derivatives g₁, …, g₄.

The series ∑ ℓ⁴ x^ℓ

noncomputable def Zeta5Irrational.Ptel (N x : ℝ) : ℝ

The telescoping polynomial: (1 - x)⁵ ∑_{ℓ < N} (ℓ+1)⁴ x^{ℓ+1} = x(1+11x+11x²+x³) - x^{N+1} P(N, x).

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta5Irrational.telescope (x : ℝ) (N : ℕ) : (1 - x) ^ 5 * ∑ ℓ ∈ Finset.range N, (↑ℓ + 1) ^ 4 * x ^ (ℓ + 1) = x * (1 + 11 * x + 11 * x ^ 2 + x ^ 3) - x ^ (N + 1) * Ptel (↑N) x

theorem Zeta5Irrational.tendsto_pow_mul_Ptel {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) : Filter.Tendsto (fun (N : ℕ) => x ^ (N + 1) * Ptel (↑N) x) Filter.atTop (nhds 0)

theorem Zeta5Irrational.hasSum_pow_four_mul_geometric {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) : HasSum (fun (ℓ : ℕ) => (↑ℓ + 1) ^ 4 * x ^ (ℓ + 1)) (x * (1 + 11 * x + 11 * x ^ 2 + x ^ 3) / (1 - x) ^ 5)

∑_{ℓ ≥ 1} ℓ⁴ x^ℓ = x (1 + 11x + 11x² + x³) / (1 - x)⁵.

F(y) = 1 / (e^{2πy} - 1) and its derivatives

noncomputable def Zeta5Irrational.qe (y : ℝ) : ℝ

q(y) = e^{2πy}.

Equations

• Zeta5Irrational.qe y = Real.exp (2 * Real.pi * y)

theorem Zeta5Irrational.qe_pos (y : ℝ) : 0 < qe y

theorem Zeta5Irrational.qe_gt_one {y : ℝ} (hy : 0 < y) : 1 < qe y

theorem Zeta5Irrational.hasDerivAt_qe (y : ℝ) : HasDerivAt qe (2 * Real.pi * qe y) y

noncomputable def Zeta5Irrational.F0 (y : ℝ) : ℝ

F(y) = 1 / (e^{2πy} - 1) and its first four derivatives.

Equations

• Zeta5Irrational.F0 y = 1 / (Zeta5Irrational.qe y - 1)

noncomputable def Zeta5Irrational.F1 (y : ℝ) : ℝ

Expression for the first derivative of F0 on the positive half-line.

Equations

• Zeta5Irrational.F1 y = -(2 * Real.pi) * Zeta5Irrational.qe y / (Zeta5Irrational.qe y - 1) ^ 2

noncomputable def Zeta5Irrational.F2 (y : ℝ) : ℝ

Expression for the second derivative of F0 on the positive half-line.

Equations

• Zeta5Irrational.F2 y = (2 * Real.pi) ^ 2 * Zeta5Irrational.qe y * (Zeta5Irrational.qe y + 1) / (Zeta5Irrational.qe y - 1) ^ 3

noncomputable def Zeta5Irrational.F3 (y : ℝ) : ℝ

Expression for the third derivative of F0 on the positive half-line.

Equations

• Zeta5Irrational.F3 y = -(2 * Real.pi) ^ 3 * Zeta5Irrational.qe y * (Zeta5Irrational.qe y ^ 2 + 4 * Zeta5Irrational.qe y + 1) / (Zeta5Irrational.qe y - 1) ^ 4

noncomputable def Zeta5Irrational.F4 (y : ℝ) : ℝ

Expression for the fourth derivative of F0 on the positive half-line.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta5Irrational.hasDerivAt_F0 {y : ℝ} (hy : 0 < y) : HasDerivAt F0 (F1 y) y

theorem Zeta5Irrational.hasDerivAt_F1 {y : ℝ} (hy : 0 < y) : HasDerivAt F1 (F2 y) y

theorem Zeta5Irrational.hasDerivAt_F2 {y : ℝ} (hy : 0 < y) : HasDerivAt F2 (F3 y) y

theorem Zeta5Irrational.hasDerivAt_F3 {y : ℝ} (hy : 0 < y) : HasDerivAt F3 (F4 y) y

theorem Zeta5Irrational.wS_eq {y : ℝ} (hy : 0 < y) : wS y = qe y * (qe y ^ 3 + 11 * qe y ^ 2 + 11 * qe y + 1) / (qe y - 1) ^ 5

The series wS in closed form: wS(y) = q (q³ + 11q² + 11q + 1) / (q - 1)⁵.

theorem Zeta5Irrational.w_eq_F4 {y : ℝ} (hy : 0 < y) : w y = y ^ 5 * F4 y / 12

w(y) = y⁵ F₄(y) / 12 for y > 0.

g(y) = y⁵ / (12 (y² + a²)) and its derivatives

noncomputable def Zeta5Irrational.g0 (a y : ℝ) : ℝ

Rational factor paired with F4 in the Hermite integral formula.

Equations

• Zeta5Irrational.g0 a y = y ^ 5 / (12 * (y ^ 2 + a ^ 2))

noncomputable def Zeta5Irrational.g1 (a y : ℝ) : ℝ

First derivative of the rational factor g0 a, for positive a.

Equations

• Zeta5Irrational.g1 a y = y ^ 4 * (5 * a ^ 2 + 3 * y ^ 2) / (12 * (y ^ 2 + a ^ 2) ^ 2)

noncomputable def Zeta5Irrational.g2 (a y : ℝ) : ℝ

Second derivative of the rational factor g0 a, for positive a.

Equations

• Zeta5Irrational.g2 a y = y ^ 3 * (10 * a ^ 4 + 9 * a ^ 2 * y ^ 2 + 3 * y ^ 4) / (6 * (y ^ 2 + a ^ 2) ^ 3)

noncomputable def Zeta5Irrational.g3 (a y : ℝ) : ℝ

Third derivative of the rational factor g0 a, for positive a.

Equations

• Zeta5Irrational.g3 a y = y ^ 2 * (10 * a ^ 6 + 5 * a ^ 4 * y ^ 2 + 4 * a ^ 2 * y ^ 4 + y ^ 6) / (2 * (y ^ 2 + a ^ 2) ^ 4)

noncomputable def Zeta5Irrational.g4 (a y : ℝ) : ℝ

Fourth derivative of the rational factor g0 a, for positive a.

Equations

• Zeta5Irrational.g4 a y = 2 * a ^ 4 * y * (5 * a ^ 4 - 10 * a ^ 2 * y ^ 2 + y ^ 4) / (y ^ 2 + a ^ 2) ^ 5

theorem Zeta5Irrational.hasDerivAt_g0 {a : ℝ} (ha : 0 < a) (y : ℝ) : HasDerivAt (g0 a) (g1 a y) y

theorem Zeta5Irrational.hasDerivAt_g1 {a : ℝ} (ha : 0 < a) (y : ℝ) : HasDerivAt (g1 a) (g2 a y) y

theorem Zeta5Irrational.hasDerivAt_g2 {a : ℝ} (ha : 0 < a) (y : ℝ) : HasDerivAt (g2 a) (g3 a y) y

theorem Zeta5Irrational.hasDerivAt_g3 {a : ℝ} (ha : 0 < a) (y : ℝ) : HasDerivAt (g3 a) (g4 a y) y

Bounds, integrability and the first integral ∫₀^∞ g₄ = 1/2

theorem Zeta5Irrational.abs_g4_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 ≤ y) : |g4 a y| ≤ 10 * a ^ 3 / (y ^ 2 + a ^ 2) ^ 2

theorem Zeta5Irrational.inv_sq_add_le {a : ℝ} (ha : 0 < a) (y : ℝ) : 1 / (y ^ 2 + a ^ 2) ≤ (1 + 1 / a ^ 2) * (1 / (1 + y ^ 2))

theorem Zeta5Irrational.integrableOn_g4 {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (g4 a) (Set.Ioi 0) MeasureTheory.volume

g₄ · h is integrable on (0, ∞) whenever h is measurable and bounded by 1/(y²+a²) -type control: we only need the three cases below.

theorem Zeta5Irrational.tendsto_g3_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (g3 a) Filter.atTop (nhds (1 / 2))

theorem Zeta5Irrational.integral_g4 {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, g4 a y = 1 / 2

∫₀^∞ g₄(y) dy = 1/2.

theorem Zeta5Irrational.F0_series {y : ℝ} (hy : 0 < y) : F0 y = -1 / 2 + 1 / (2 * Real.pi * y) + 1 / Real.pi * ∑' (n : ℕ), y / (y ^ 2 + (↑n + 1) ^ 2)

The Mittag-Leffler expansion of F(y) = 1/(e^{2πy} - 1): F(y) = -1/2 + 1/(2πy) + (1/π) ∑_{n ≥ 1} y/(y² + n²), from Mathlib's cot_series_rep.