← Copula mathematical handbook

The polynomial coefficient branch and the exact maximum gap

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_blest_noise (b : ℝ) (hb : 0 ≤ b) : blestNu (extremalCopula b hb) = (12 * ∫ (p : ↑unitInterval × ↑unitInterval), Support.squarePotential p.2 * Support.noiseMoment 1 (b * Support.squareDelta p)) - 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_coefficients_polynomial (b : ℝ) (hb : b ∈ Set.Icc 0 1) : (extremalCopula b ⋯).chatterjeeXi = 8 * b ^ 2 * (7 - 3 * b) / 105 ∧ blestNu (extremalCopula b ⋯) = 4 * b * (28 - 9 * b) / 105

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_one_coefficients : (extremalCopula 1 ⋯).chatterjeeXi = 32 / 105 ∧ blestNu (extremalCopula 1 ⋯) = 76 / 105

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.maximal_signed_gap (C : Copula 2) : blestNu C - C.chatterjeeXi ≤ 44 / 105

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.maximal_signed_gap_eq_iff (C : Copula 2) : blestNu C - C.chatterjeeXi = 44 / 105 ↔ C = extremalCopula 1 ⋯

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.maximal_absolute_gap (C : Copula 2) : |blestNu C| - C.chatterjeeXi ≤ 44 / 105

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.maximal_absolute_gap_eq_iff (C : Copula 2) : |blestNu C| - C.chatterjeeXi = 44 / 105 ↔ C = extremalCopula 1 ⋯ ∨ C = (extremalCopula 1 ⋯).reflect {1}