← Copula mathematical handbook

Spearman's rho: distance formulas, bounds and benchmark copulas

theorem ProbabilityTheory.Copula.spearmanRho_eq_one_sub (C : Copula 2) : C.spearmanRho = 1 - 6 * ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂C.toMeasure

theorem ProbabilityTheory.Copula.spearmanRho_eq_neg_one_add (C : Copula 2) : C.spearmanRho = -1 + 6 * ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) + ↑(x 1) - 1) ^ 2 ∂C.toMeasure

theorem ProbabilityTheory.Copula.spearmanRho_mem_Icc (C : Copula 2) : C.spearmanRho ∈ Set.Icc (-1) 1

@[simp]

theorem ProbabilityTheory.Copula.spearmanRho_independence : (independence 2).spearmanRho = 0

@[simp]

theorem ProbabilityTheory.Copula.spearmanRho_comonotonic : (comonotonic 2).spearmanRho = 1

@[simp]

theorem ProbabilityTheory.Copula.spearmanRho_countermonotonic : countermonotonic.spearmanRho = -1