← Copula mathematical handbook

The bivariate concordance function

The symmetric function Q(C,D) = 4 ∫ C dD - 1 polarizes Kendall's tau. Pairing with independence recovers one third of Spearman's rho, while the two Fréchet bounds connect it with footrule and Gini's gamma.

noncomputable def ProbabilityTheory.Copula.concordanceQ (C D : Copula 2) : ℝ

The concordance function of two bivariate copulas.

Equations

• C.concordanceQ D = 4 * ∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂D.toMeasure - 1

theorem ProbabilityTheory.Copula.concordanceQ_comm (C D : Copula 2) : C.concordanceQ D = D.concordanceQ C

@[simp]

theorem ProbabilityTheory.Copula.concordanceQ_self (C : Copula 2) : C.concordanceQ C = C.kendallTau

theorem ProbabilityTheory.Copula.concordanceQ_mem_Icc (C D : Copula 2) : C.concordanceQ D ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.LowerOrthantLE.concordanceQ_le_left {C D : Copula 2} (h : C.LowerOrthantLE D) (E : Copula 2) : C.concordanceQ E ≤ D.concordanceQ E

theorem ProbabilityTheory.Copula.LowerOrthantLE.concordanceQ_le_right {C D : Copula 2} (h : C.LowerOrthantLE D) (E : Copula 2) : E.concordanceQ C ≤ E.concordanceQ D

theorem ProbabilityTheory.Copula.concordanceQ_independence (C : Copula 2) : C.concordanceQ (independence 2) = C.spearmanRho / 3

theorem ProbabilityTheory.Copula.concordanceQ_comonotonic (C : Copula 2) : C.concordanceQ (comonotonic 2) = (2 * C.spearmanFootrule + 1) / 3

theorem ProbabilityTheory.Copula.concordanceQ_countermonotonic (C : Copula 2) : C.concordanceQ countermonotonic = C.giniGamma - (2 * C.spearmanFootrule + 1) / 3

theorem ProbabilityTheory.Copula.giniGamma_eq_concordanceQ (C : Copula 2) : C.giniGamma = C.concordanceQ (comonotonic 2) + C.concordanceQ countermonotonic

@[simp]

theorem ProbabilityTheory.Copula.concordanceQ_comonotonic_countermonotonic : (comonotonic 2).concordanceQ countermonotonic = 0

theorem ProbabilityTheory.Copula.concordanceQ_finiteMixture_left {n : ℕ} (C : Fin n → Copula 2) (w : Fin n → ℝ) (hw : ∀ (j : Fin n), 0 ≤ w j) (hsum : ∑ j : Fin n, w j = 1) (D : Copula 2) : (finiteMixture C w hw hsum).concordanceQ D = ∑ j : Fin n, w j * (C j).concordanceQ D

theorem ProbabilityTheory.Copula.concordanceQ_finiteMixture_right {n : ℕ} (C : Fin n → Copula 2) (w : Fin n → ℝ) (hw : ∀ (j : Fin n), 0 ≤ w j) (hsum : ∑ j : Fin n, w j = 1) (D : Copula 2) : D.concordanceQ (finiteMixture C w hw hsum) = ∑ j : Fin n, w j * D.concordanceQ (C j)

theorem ProbabilityTheory.Copula.concordanceQ_mix_left (C D E : Copula 2) (a : ↑unitInterval) : (C.mix D a).concordanceQ E = ↑a * C.concordanceQ E + (1 - ↑a) * D.concordanceQ E

theorem ProbabilityTheory.Copula.concordanceQ_mix_right (C D E : Copula 2) (a : ↑unitInterval) : C.concordanceQ (D.mix E a) = ↑a * C.concordanceQ D + (1 - ↑a) * C.concordanceQ E