← Copula mathematical handbook

The entire vertical boundary in Theorem 1.1

On radially symmetric copulas Blest's nu equals Spearman's rho. The centered deterministic witnesses therefore cover nu in [-1,1] while keeping xi=1.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_eq_rho_of_radiallySymmetric (C : Copula 2) (hC : C.IsRadiallySymmetric) : blestNu C = C.spearmanRho

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.xi_one_slice (v : ℝ) : (∃ (C : Copula 2), C.chatterjeeXi = 1 ∧ blestNu C = v) ↔ v ∈ Set.Icc (-1) 1