The rational integrals in Hermite's formula

• ∫₀^∞ g₄(y)/y dy = π/a;
• ∫₀^∞ g₄(y) y/(y² + n²) dy = π a⁴/(a + n)⁵ for n > 0 (separate closed forms for n ≠ a and n = a). The antiderivatives (a rational function plus arctan terms) are verified by differentiation.

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

g₄(y) / y as a rational function (continuous at 0).

Equations

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

theorem Zeta5Irrational.g4_div_eq_h4 (a : ℝ) {y : ℝ} (hy : y ≠ 0) : g4 a y / y = h4 a y

theorem Zeta5Irrational.abs_h4_le {a : ℝ} (ha : 0 < a) (y : ℝ) : |h4 a y| ≤ 20 / (y ^ 2 + a ^ 2)

theorem Zeta5Irrational.integrableOn_of_le_inv_sq {a : ℝ} (ha : 0 < a) {f : ℝ → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))) {C : ℝ} (hC : ∀ (y : ℝ), 0 < y → |f y| ≤ C / (y ^ 2 + a ^ 2)) : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume

theorem Zeta5Irrational.tendsto_arctan_div_atTop {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (y : ℝ) => Real.arctan (y / c)) Filter.atTop (nhds (Real.pi / 2))

The limit arctan (y / c) → π/2 as y → ∞, for c > 0.

∫₀^∞ g₄(y)/y dy = π / a

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

Antiderivative of h₄.

Equations

• Zeta5Irrational.A1 a y = 2 / a * Real.arctan (y / a) + 2 * y * (12 * a ^ 6 + 14 * a ^ 4 * y ^ 2 + 11 * a ^ 2 * y ^ 4 + 3 * y ^ 6) / (3 * (a ^ 2 + y ^ 2) ^ 4)

theorem Zeta5Irrational.hasDerivAt_A1 {a : ℝ} (ha : 0 < a) (y : ℝ) : HasDerivAt (A1 a) (h4 a y) y

theorem Zeta5Irrational.tendsto_A1_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (A1 a) Filter.atTop (nhds (Real.pi / a))

theorem Zeta5Irrational.continuous_g4 (a : ℝ) (ha : 0 < a) : Continuous (g4 a)

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

theorem Zeta5Irrational.integral_h4 {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, h4 a y = Real.pi / a

∫₀^∞ g₄(y)/y dy = π/a.

∫₀^∞ g₄(y) y/(y² + n²) dy = π a⁴/(a + n)⁵

noncomputable def Zeta5Irrational.k4 (a n y : ℝ) : ℝ

The integrand g₄(y) · y/(y² + n²).

Equations

• Zeta5Irrational.k4 a n y = Zeta5Irrational.g4 a y * (y / (y ^ 2 + n ^ 2))

theorem Zeta5Irrational.abs_k4_le {a n : ℝ} (ha : 0 < a) (hn : 0 < n) {y : ℝ} (hy : 0 < y) : |k4 a n y| ≤ 5 * a / n / (y ^ 2 + a ^ 2)

theorem Zeta5Irrational.integrableOn_k4 {a n : ℝ} (ha : 0 < a) (hn : 0 < n) : MeasureTheory.IntegrableOn (k4 a n) (Set.Ioi 0) MeasureTheory.volume

noncomputable def Zeta5Irrational.A2 (a n y : ℝ) : ℝ

Antiderivative of k4 a n for n ≠ a; D = a² - n².

Equations

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

theorem Zeta5Irrational.hasDerivAt_A2 {a n : ℝ} (ha : 0 < a) (hn : 0 < n) (hne : n ≠ a) (y : ℝ) : HasDerivAt (A2 a n) (k4 a n y) y

theorem Zeta5Irrational.tendsto_A2_atTop {a n : ℝ} (ha : 0 < a) (hn : 0 < n) (hne : n ≠ a) : Filter.Tendsto (A2 a n) Filter.atTop (nhds (Real.pi * a ^ 4 / (a + n) ^ 5))

theorem Zeta5Irrational.integral_k4_ne {a n : ℝ} (ha : 0 < a) (hn : 0 < n) (hne : n ≠ a) : ∫ (y : ℝ) in Set.Ioi 0, k4 a n y = Real.pi * a ^ 4 / (a + n) ^ 5

∫₀^∞ g₄(y) y/(y² + n²) dy = π a⁴/(a + n)⁵ for n ≠ a.

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

Antiderivative of k4 a a.

Equations

• Zeta5Irrational.A2e a y = Real.arctan (y / a) / (16 * a) + y * (-15 * a ^ 8 + 730 * a ^ 6 * y ^ 2 + 32 * a ^ 4 * y ^ 4 + 70 * a ^ 2 * y ^ 6 + 15 * y ^ 8) / (240 * (a ^ 2 + y ^ 2) ^ 5)

theorem Zeta5Irrational.hasDerivAt_A2e {a : ℝ} (ha : 0 < a) (y : ℝ) : HasDerivAt (A2e a) (k4 a a y) y

theorem Zeta5Irrational.tendsto_A2e_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (A2e a) Filter.atTop (nhds (Real.pi * a ^ 4 / (a + a) ^ 5))

theorem Zeta5Irrational.integral_k4_eq {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, k4 a a y = Real.pi * a ^ 4 / (a + a) ^ 5

∫₀^∞ g₄(y) y/(y² + a²) dy = π a⁴/(2a)⁵.

theorem Zeta5Irrational.integral_k4 {a n : ℝ} (ha : 0 < a) (hn : 0 < n) : ∫ (y : ℝ) in Set.Ioi 0, k4 a n y = Real.pi * a ^ 4 / (a + n) ^ 5

∫₀^∞ g₄(y) y/(y² + n²) dy = π a⁴/(a + n)⁵ for all n > 0.