Exact tail integrals in terms of four radical moments #
theorem
Verification.integral_xiTail_radical
(b r : ℝ)
(hb : 0 < b)
(hr : r ∈ Set.Ioo 0 1)
(hbr : b * r ^ 2 = 1)
:
∫ (p : ↑unitInterval × ↑unitInterval), xiTail b |squareDelta p| = 2 * (radicalMoment r 0 + -3 * b ^ 2 * (8 * radicalMoment r 2 + 4 * r ^ 2 * radicalMoment r 1 + 3 * r ^ 4 * radicalMoment r 0) / 15 + 2 * b ^ 3 * (16 * radicalMoment r 3 + 8 * r ^ 2 * radicalMoment r 2 + 6 * r ^ 4 * radicalMoment r 1 + 5 * r ^ 6 * radicalMoment r 0) / 35)
theorem
Verification.integral_nuTail_radical
(b r : ℝ)
(hb : 0 < b)
(hr : r ∈ Set.Ioo 0 1)
(hbr : b * r ^ 2 = 1)
:
∫ (p : ↑unitInterval × ↑unitInterval), nuTail b |squareDelta p| = 2 * (3 * (2 * radicalMoment r 1 + r ^ 2 * radicalMoment r 0) / 3 + -6 * b * (8 * radicalMoment r 2 + 4 * r ^ 2 * radicalMoment r 1 + 3 * r ^ 4 * radicalMoment r 0) / 15 + 3 * b ^ 2 * (16 * radicalMoment r 3 + 8 * r ^ 2 * radicalMoment r 2 + 6 * r ^ 4 * radicalMoment r 1 + 5 * r ^ 6 * radicalMoment r 0) / 35)