← Mathematical handbook

Equality cases for population rank coefficients

Rho, tau and gamma attain their upper and lower bounds only at the corresponding Fréchet copulas. Footrule attains its upper bound only at comonotonicity; its lower bound characterizes the diagonal section instead.

theorem ProbabilityTheory.Copula.spearmanRho_eq_one_iff (C : Copula 2) : C.spearmanRho = 1 ↔ C = comonotonic 2

theorem ProbabilityTheory.Copula.spearmanRho_eq_neg_one_iff (C : Copula 2) : C.spearmanRho = -1 ↔ C = countermonotonic

theorem ProbabilityTheory.Copula.kendallTau_eq_one_iff (C : Copula 2) : C.kendallTau = 1 ↔ C = comonotonic 2

theorem ProbabilityTheory.Copula.kendallTau_eq_neg_one_iff (C : Copula 2) : C.kendallTau = -1 ↔ C = countermonotonic

theorem ProbabilityTheory.Copula.spearmanFootrule_eq_one_iff (C : Copula 2) : C.spearmanFootrule = 1 ↔ C = comonotonic 2

theorem ProbabilityTheory.Copula.spearmanFootrule_eq_neg_half_iff (C : Copula 2) : C.spearmanFootrule = -1 / 2 ↔ ∀ (t : ↑unitInterval), C.diagonal t = max 0 (2 * ↑t - 1)

theorem ProbabilityTheory.Copula.giniGamma_eq_one_iff (C : Copula 2) : C.giniGamma = 1 ↔ C = comonotonic 2

theorem ProbabilityTheory.Copula.giniGamma_eq_neg_one_iff (C : Copula 2) : C.giniGamma = -1 ↔ C = countermonotonic

theorem ProbabilityTheory.Copula.spearmanRho_lt_one_iff (C : Copula 2) : C.spearmanRho < 1 ↔ C ≠ comonotonic 2

theorem ProbabilityTheory.Copula.neg_one_lt_spearmanRho_iff (C : Copula 2) : -1 < C.spearmanRho ↔ C ≠ countermonotonic

theorem ProbabilityTheory.Copula.kendallTau_lt_one_iff (C : Copula 2) : C.kendallTau < 1 ↔ C ≠ comonotonic 2

theorem ProbabilityTheory.Copula.neg_one_lt_kendallTau_iff (C : Copula 2) : -1 < C.kendallTau ↔ C ≠ countermonotonic

theorem ProbabilityTheory.Copula.spearmanFootrule_lt_one_iff (C : Copula 2) : C.spearmanFootrule < 1 ↔ C ≠ comonotonic 2

theorem ProbabilityTheory.Copula.giniGamma_lt_one_iff (C : Copula 2) : C.giniGamma < 1 ↔ C ≠ comonotonic 2

theorem ProbabilityTheory.Copula.neg_one_lt_giniGamma_iff (C : Copula 2) : -1 < C.giniGamma ↔ C ≠ countermonotonic