← Copula mathematical handbook

Every rho is attained at xi=1 by a radially symmetric copula

theorem ProbabilityTheory.Copula.RankRegion.Common.centralW_rho (α : ↑unitInterval) : (centralW α).spearmanRho = 1 - 2 * ↑α ^ 3

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