← Mathematical handbook

The one-dimensional coefficient integrals in Lemma 4.1

noncomputable def Papers.Rockel2026XiBlest.sectionSquare (b q : ℝ) : ℝ

Equations

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

noncomputable def Papers.Rockel2026XiBlest.sectionWeighted (b q : ℝ) : ℝ

Equations

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

theorem Papers.Rockel2026XiBlest.continuous_sectionSquare (b : ℝ) : Continuous (sectionSquare b)

theorem Papers.Rockel2026XiBlest.continuous_sectionWeighted (b : ℝ) : Continuous (sectionWeighted b)

theorem Papers.Rockel2026XiBlest.one_dimensional_coefficients (b : ℝ) (hb : 0 < b) : (extremalCopula b ⋯).chatterjeeXi = (6 * ∫ (q : ℝ) in -1 / b..1, sectionSquare b q * -deriv (normalizationMean b) q) - 2 ∧ blestNu (extremalCopula b ⋯) = (12 * ∫ (q : ℝ) in -1 / b..1, sectionWeighted b q * -deriv (normalizationMean b) q) - 2

Equations (23)-(24), with the derivative of the actual normalization map.

theorem Papers.Rockel2026XiBlest.lower_square_polynomial (r : ℝ) : Verification.quadraticF (r ^ 2) 1 - Verification.quadraticF (r ^ 2) r = 1 / 5 - 2 * r ^ 2 / 3 + r ^ 4 - 8 * r ^ 5 / 15

Correct expansion of the lower-clamped square moment.

theorem Papers.Rockel2026XiBlest.printed_lower_square_polynomial_false : Verification.quadraticF ((1 / 2) ^ 2) 1 - Verification.quadraticF ((1 / 2) ^ 2) (1 / 2) ≠ 1 / 5 - 2 * (1 / 2) ^ 2 / 3 + (1 / 2) ^ 4 - (1 / 2) ^ 5 / 5

The preprint's displayed G_iv polynomial omits part of F(r;r^2).