← Mathematical handbook

Closed hyperbolic expressions for both extremal coefficient integrals

theorem Verification.xi_hyperbolic_integral (b r : ℝ) (hb : 0 < b) (hr : r ∈ Set.Ioo 0 1) (hbr : b * r ^ 2 = 1) : 8 * b ^ 2 * (7 - 3 * b) / 105 + ∫ (p : ↑unitInterval × ↑unitInterval), xiTail b |squareDelta p| = (183 * √(1 - r ^ 2) - 38 * b * √(1 - r ^ 2) - 88 * b ^ 2 * √(1 - r ^ 2) + 112 * b ^ 2 + 48 * b ^ 3 * √(1 - r ^ 2) - 48 * b ^ 3 - 105 * Real.arcosh (1 / r) / b) / 210

theorem Verification.nu_hyperbolic_integral (b r : ℝ) (hb : 0 < b) (hr : r ∈ Set.Ioo 0 1) (hbr : b * r ^ 2 = 1) : 4 * b * (28 - 9 * b) / 105 + ∫ (p : ↑unitInterval × ↑unitInterval), nuTail b |squareDelta p| = (87 * √(1 - r ^ 2) / b + 250 * √(1 - r ^ 2) - 376 * b * √(1 - r ^ 2) + 448 * b + 144 * b ^ 2 * √(1 - r ^ 2) - 144 * b ^ 2 - 105 * Real.arcosh (1 / r) / b ^ 2) / 420