← Copula mathematical handbook

Rank coefficients of binary ordinal sums

The deficits from one scale cubically for Spearman's rho and quadratically for Kendall's tau and Spearman's footrule. A more general identity gives concordance between two ordinal sums with the same split. Every formula includes the endpoint splits and singular component copulas.

theorem ProbabilityTheory.Copula.cdf_ordinalSum_lowerEmbed_vec (C D : Copula 2) (a : ↑unitInterval) (x : Fin 2 → ↑unitInterval) (ha : 0 < a) : ((C.ordinalSum D a).cdf fun (i : Fin 2) => OrdinalSum.lowerEmbed a (x i)) = ↑a * C.cdf x

theorem ProbabilityTheory.Copula.cdf_ordinalSum_upperEmbed_vec (C D : Copula 2) (a : ↑unitInterval) (x : Fin 2 → ↑unitInterval) (ha : a < 1) : ((C.ordinalSum D a).cdf fun (i : Fin 2) => OrdinalSum.upperEmbed a (x i)) = ↑a + (1 - ↑a) * D.cdf x

theorem ProbabilityTheory.Copula.concordanceQ_ordinalSum (C D E F : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).concordanceQ (E.ordinalSum F a) = 1 - ↑a ^ 2 * (1 - C.concordanceQ E) - (1 - ↑a) ^ 2 * (1 - D.concordanceQ F)

Concordance of two ordinal sums with a common split.

theorem ProbabilityTheory.Copula.kendallTau_ordinalSum (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).kendallTau = 1 - ↑a ^ 2 * (1 - C.kendallTau) - (1 - ↑a) ^ 2 * (1 - D.kendallTau)

theorem ProbabilityTheory.Copula.spearmanFootrule_ordinalSum (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).spearmanFootrule = 1 - ↑a ^ 2 * (1 - C.spearmanFootrule) - (1 - ↑a) ^ 2 * (1 - D.spearmanFootrule)

theorem ProbabilityTheory.Copula.spearmanRho_ordinalSum (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).spearmanRho = 1 - ↑a ^ 3 * (1 - C.spearmanRho) - (1 - ↑a) ^ 3 * (1 - D.spearmanRho)