← Mathematical handbook

Radical moments underlying the hyperbolic coefficient branch

theorem Verification.hasDerivAt_arcosh_scaled {r x : ℝ} (hr : 0 < r) (hx : r < x) : HasDerivAt (fun (t : ℝ) => Real.arcosh (t / r)) (1 / √(x ^ 2 - r ^ 2)) x

theorem Verification.hasDerivAt_sqrt_square_sub {r x : ℝ} (hr : 0 < r) (hx : r < x) : HasDerivAt (fun (t : ℝ) => √(t ^ 2 - r ^ 2)) (x / √(x ^ 2 - r ^ 2)) x

theorem Verification.hasDerivAt_hyperbolic_primitive {r x : ℝ} (hr : 0 < r) (hx : r < x) : HasDerivAt (fun (t : ℝ) => (t * √(t ^ 2 - r ^ 2) - r ^ 2 * Real.arcosh (t / r)) / 2) (√(x ^ 2 - r ^ 2)) x

noncomputable def Verification.radicalMoment (r : ℝ) (k : ℕ) : ℝ

Equations

• Verification.radicalMoment r k = ∫ (x : ℝ) in r..1, x ^ (2 * k) * √(x ^ 2 - r ^ 2)

theorem Verification.radicalMoment_zero (r : ℝ) (hr : r ∈ Set.Ioo 0 1) : radicalMoment r 0 = (√(1 - r ^ 2) - r ^ 2 * Real.arcosh (1 / r)) / 2

theorem Verification.hasDerivAt_radical_recurrence {r x : ℝ} (hr : 0 < r) (hx : r < x) (n : ℕ) : HasDerivAt (fun (t : ℝ) => t ^ (2 * n + 1) * √(t ^ 2 - r ^ 2) ^ 3) ((2 * ↑n + 4) * x ^ (2 * (n + 1)) * √(x ^ 2 - r ^ 2) - (2 * ↑n + 1) * r ^ 2 * x ^ (2 * n) * √(x ^ 2 - r ^ 2)) x

theorem Verification.radicalMoment_recurrence (r : ℝ) (hr : r ∈ Set.Ioo 0 1) (n : ℕ) : (2 * ↑n + 4) * radicalMoment r (n + 1) - (2 * ↑n + 1) * r ^ 2 * radicalMoment r n = √(1 - r ^ 2) ^ 3