← Copula mathematical handbook

The entire vertical boundary in Theorem 1

theorem ProbabilityTheory.Copula.RankRegion.XiRho.xi_one_slice (r : ℝ) : (∃ (C : Copula 2), C.chatterjeeXi = 1 ∧ C.spearmanRho = r) ↔ r ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.RankRegion.XiRho.symmetric_xi_one_attained (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) : ∃ (C : Copula 2), C.IsRadiallySymmetric ∧ C.chatterjeeXi = 1 ∧ C.spearmanRho = r