← Copula mathematical handbook

Sharp bounds and explicit ordinal-sum rank formulas

Two independent components yield positive rank dependence at every interior split, maximized uniquely by equal block lengths. Two countermonotonic components attain the sharp lower bounds at each fixed split.

theorem ProbabilityTheory.Copula.kendallTau_ordinalSum_independence (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).kendallTau = 2 * ↑a * (1 - ↑a)

theorem ProbabilityTheory.Copula.spearmanRho_ordinalSum_independence (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).spearmanRho = 3 * ↑a * (1 - ↑a)

theorem ProbabilityTheory.Copula.spearmanFootrule_ordinalSum_independence (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).spearmanFootrule = 2 * ↑a * (1 - ↑a)

theorem ProbabilityTheory.Copula.kendallTau_ordinalSum_countermonotonic (a : ↑unitInterval) : (countermonotonic.ordinalSum countermonotonic a).kendallTau = 4 * ↑a * (1 - ↑a) - 1

theorem ProbabilityTheory.Copula.spearmanRho_ordinalSum_countermonotonic (a : ↑unitInterval) : (countermonotonic.ordinalSum countermonotonic a).spearmanRho = 6 * ↑a * (1 - ↑a) - 1

theorem ProbabilityTheory.Copula.spearmanFootrule_ordinalSum_countermonotonic (a : ↑unitInterval) : (countermonotonic.ordinalSum countermonotonic a).spearmanFootrule = 3 * ↑a * (1 - ↑a) - 1 / 2

theorem ProbabilityTheory.Copula.kendallTau_ordinalSum_lower_bound (C D : Copula 2) (a : ↑unitInterval) : 4 * ↑a * (1 - ↑a) - 1 ≤ (C.ordinalSum D a).kendallTau

The sharp lower bound for tau at a fixed split.

theorem ProbabilityTheory.Copula.spearmanRho_ordinalSum_lower_bound (C D : Copula 2) (a : ↑unitInterval) : 6 * ↑a * (1 - ↑a) - 1 ≤ (C.ordinalSum D a).spearmanRho

The sharp lower bound for rho at a fixed split.

theorem ProbabilityTheory.Copula.spearmanFootrule_ordinalSum_lower_bound (C D : Copula 2) (a : ↑unitInterval) : 3 * ↑a * (1 - ↑a) - 1 / 2 ≤ (C.ordinalSum D a).spearmanFootrule

The sharp lower bound for footrule at a fixed split.

theorem ProbabilityTheory.Copula.kendallTau_ordinalSum_independence_le_half (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).kendallTau ≤ 1 / 2

theorem ProbabilityTheory.Copula.spearmanRho_ordinalSum_independence_le_three_quarters (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).spearmanRho ≤ 3 / 4

theorem ProbabilityTheory.Copula.spearmanFootrule_ordinalSum_independence_le_half (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).spearmanFootrule ≤ 1 / 2

theorem ProbabilityTheory.Copula.kendallTau_ordinalSum_independence_eq_half_iff (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).kendallTau = 1 / 2 ↔ a = unitHalf

theorem ProbabilityTheory.Copula.spearmanRho_ordinalSum_independence_eq_three_quarters_iff (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).spearmanRho = 3 / 4 ↔ a = unitHalf

theorem ProbabilityTheory.Copula.spearmanFootrule_ordinalSum_independence_eq_half_iff (a : ↑unitInterval) : ((independence 2).ordinalSum (independence 2) a).spearmanFootrule = 1 / 2 ↔ a = unitHalf