← Mathematical handbook

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

theorem Verification.centralW_rho (α : ↑unitInterval) : (centralW α).spearmanRho = 1 - 2 * ↑α ^ 3

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