← Copula mathematical handbook

Strict concordance monotonicity of Spearman's rho

Among two comparable copulas, equality of rho forces equality of the copulas. In particular, zero rho detects independence within either the PQD or NQD class. No such claim is made for arbitrary copulas.

theorem ProbabilityTheory.Copula.LowerOrthantLE.spearmanRho_eq_iff {C D : Copula 2} (h : C.LowerOrthantLE D) : C.spearmanRho = D.spearmanRho ↔ C = D

theorem ProbabilityTheory.Copula.LowerOrthantLE.spearmanRho_lt_iff {C D : Copula 2} (h : C.LowerOrthantLE D) : C.spearmanRho < D.spearmanRho ↔ C ≠ D

theorem ProbabilityTheory.Copula.LowerOrthantLE.spearmanRho_lt {C D : Copula 2} (h : C.LowerOrthantLE D) (hne : C ≠ D) : C.spearmanRho < D.spearmanRho

theorem ProbabilityTheory.Copula.ConcordanceLE.spearmanRho_eq_iff {C D : Copula 2} (h : C.ConcordanceLE D) : C.spearmanRho = D.spearmanRho ↔ C = D

theorem ProbabilityTheory.Copula.ConcordanceLE.spearmanRho_lt_iff {C D : Copula 2} (h : C.ConcordanceLE D) : C.spearmanRho < D.spearmanRho ↔ C ≠ D

theorem ProbabilityTheory.Copula.isNQD_iff_lowerOrthantLE (C : Copula 2) : C.IsNQD ↔ C.LowerOrthantLE (independence 2)

theorem ProbabilityTheory.Copula.IsPQD.spearmanRho_eq_zero_iff {C : Copula 2} (h : C.IsPQD) : C.spearmanRho = 0 ↔ C = independence 2

theorem ProbabilityTheory.Copula.IsNQD.spearmanRho_eq_zero_iff {C : Copula 2} (h : C.IsNQD) : C.spearmanRho = 0 ↔ C = independence 2

theorem ProbabilityTheory.Copula.IsPQD.spearmanRho_pos_iff {C : Copula 2} (h : C.IsPQD) : 0 < C.spearmanRho ↔ C ≠ independence 2

theorem ProbabilityTheory.Copula.IsNQD.spearmanRho_neg_iff {C : Copula 2} (h : C.IsNQD) : C.spearmanRho < 0 ↔ C ≠ independence 2

theorem ProbabilityTheory.Copula.IsPQD.kendallTau_eq_zero_iff {C : Copula 2} (h : C.IsPQD) : C.kendallTau = 0 ↔ C = independence 2

theorem ProbabilityTheory.Copula.IsPQD.kendallTau_pos_iff {C : Copula 2} (h : C.IsPQD) : 0 < C.kendallTau ↔ C ≠ independence 2

theorem ProbabilityTheory.Copula.IsNQD.spearmanRho_nonpos {C : Copula 2} (h : C.IsNQD) : C.spearmanRho ≤ 0

theorem ProbabilityTheory.Copula.IsNQD.three_mul_kendallTau_le_spearmanRho {C : Copula 2} (h : C.IsNQD) : 3 * C.kendallTau ≤ C.spearmanRho

theorem ProbabilityTheory.Copula.IsNQD.kendallTau_nonpos {C : Copula 2} (h : C.IsNQD) : C.kendallTau ≤ 0

theorem ProbabilityTheory.Copula.IsNQD.kendallTau_eq_zero_iff {C : Copula 2} (h : C.IsNQD) : C.kendallTau = 0 ↔ C = independence 2

theorem ProbabilityTheory.Copula.IsNQD.kendallTau_neg_iff {C : Copula 2} (h : C.IsNQD) : C.kendallTau < 0 ↔ C ≠ independence 2