← Copula mathematical handbook

Concordant and discordant independent pairs

For independent vectors with copulas C and D, the concordance function is the probability of concordance minus the probability of discordance. Uniform marginals exclude coordinate ties even for singular copulas. Taking C = D gives Kendall's probabilistic interpretation.

def ProbabilityTheory.Copula.concordantPairs : Set ((Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval))

Pairs whose two coordinate differences have the same strict sign.

Equations

• ProbabilityTheory.Copula.concordantPairs = {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | 0 < (↑(p.1 0) - ↑(p.2 0)) * (↑(p.1 1) - ↑(p.2 1))}

def ProbabilityTheory.Copula.discordantPairs : Set ((Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval))

Pairs whose two coordinate differences have opposite strict signs.

Equations

• ProbabilityTheory.Copula.discordantPairs = {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | (↑(p.1 0) - ↑(p.2 0)) * (↑(p.1 1) - ↑(p.2 1)) < 0}

theorem ProbabilityTheory.Copula.measurableSet_concordantPairs : MeasurableSet concordantPairs

theorem ProbabilityTheory.Copula.measurableSet_discordantPairs : MeasurableSet discordantPairs

theorem ProbabilityTheory.Copula.ae_prod_eval_ne (C D : Copula 2) (i : Fin 2) : ∀ᵐ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) ∂C.toMeasure.prod D.toMeasure, p.1 i ≠ p.2 i

theorem ProbabilityTheory.Copula.measureReal_pairs_le (C D : Copula 2) : (C.toMeasure.prod D.toMeasure).real {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | p.1 ≤ p.2} = ∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂D.toMeasure

theorem ProbabilityTheory.Copula.measureReal_pairs_ge (C D : Copula 2) : (C.toMeasure.prod D.toMeasure).real {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | p.2 ≤ p.1} = ∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂D.toMeasure

theorem ProbabilityTheory.Copula.measureReal_concordantPairs (C D : Copula 2) : (C.toMeasure.prod D.toMeasure).real concordantPairs = (1 + C.concordanceQ D) / 2

theorem ProbabilityTheory.Copula.measureReal_discordantPairs (C D : Copula 2) : (C.toMeasure.prod D.toMeasure).real discordantPairs = (1 - C.concordanceQ D) / 2

theorem ProbabilityTheory.Copula.measureReal_concordant_add_discordant (C D : Copula 2) : (C.toMeasure.prod D.toMeasure).real concordantPairs + (C.toMeasure.prod D.toMeasure).real discordantPairs = 1

theorem ProbabilityTheory.Copula.concordanceQ_eq_concordant_sub_discordant (C D : Copula 2) : C.concordanceQ D = (C.toMeasure.prod D.toMeasure).real concordantPairs - (C.toMeasure.prod D.toMeasure).real discordantPairs

theorem ProbabilityTheory.Copula.kendallTau_eq_concordant_sub_discordant (C : Copula 2) : C.kendallTau = (C.toMeasure.prod C.toMeasure).real concordantPairs - (C.toMeasure.prod C.toMeasure).real discordantPairs

Kendall's tau is concordance probability minus discordance probability for two independent observations from the copula.

theorem ProbabilityTheory.Copula.concordanceQ_eq_one_iff (C D : Copula 2) : C.concordanceQ D = 1 ↔ ∀ᵐ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) ∂C.toMeasure.prod D.toMeasure, p ∈ concordantPairs

theorem ProbabilityTheory.Copula.concordanceQ_eq_neg_one_iff (C D : Copula 2) : C.concordanceQ D = -1 ↔ ∀ᵐ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) ∂C.toMeasure.prod D.toMeasure, p ∈ discordantPairs

theorem ProbabilityTheory.Copula.kendallTau_eq_one_iff_ae_concordant (C : Copula 2) : C.kendallTau = 1 ↔ ∀ᵐ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) ∂C.toMeasure.prod C.toMeasure, p ∈ concordantPairs

theorem ProbabilityTheory.Copula.kendallTau_eq_neg_one_iff_ae_discordant (C : Copula 2) : C.kendallTau = -1 ↔ ∀ᵐ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) ∂C.toMeasure.prod C.toMeasure, p ∈ discordantPairs

theorem ProbabilityTheory.Copula.kendallTau_eq_zero_iff_balanced (C : Copula 2) : C.kendallTau = 0 ↔ (C.toMeasure.prod C.toMeasure).real concordantPairs = (C.toMeasure.prod C.toMeasure).real discordantPairs