← Mathematical handbook

Integrating the four square-gap moments

theorem Verification.integral_radical_polynomial (r a b c d : ℝ) : ∫ (x : ℝ) in r..1, (a + b * x ^ 2 + c * x ^ 4 + d * x ^ 6) * √(x ^ 2 - r ^ 2) = a * radicalMoment r 0 + b * radicalMoment r 1 + c * radicalMoment r 2 + d * radicalMoment r 3

theorem Verification.integrated_innerSquareMoment (r : ℝ) (hr : r ∈ Set.Ioo 0 1) : ∫ (x : ℝ) in r..1, innerSquareMoment x (√(x ^ 2 - r ^ 2)) 0 = radicalMoment r 0 ∧ ∫ (x : ℝ) in r..1, innerSquareMoment x (√(x ^ 2 - r ^ 2)) 1 = (2 * radicalMoment r 1 + r ^ 2 * radicalMoment r 0) / 3 ∧ ∫ (x : ℝ) in r..1, innerSquareMoment x (√(x ^ 2 - r ^ 2)) 2 = (8 * radicalMoment r 2 + 4 * r ^ 2 * radicalMoment r 1 + 3 * r ^ 4 * radicalMoment r 0) / 15 ∧ ∫ (x : ℝ) in r..1, innerSquareMoment x (√(x ^ 2 - r ^ 2)) 3 = (16 * radicalMoment r 3 + 8 * r ^ 2 * radicalMoment r 2 + 6 * r ^ 4 * radicalMoment r 1 + 5 * r ^ 6 * radicalMoment r 0) / 35