← Copula mathematical handbook

Universal Kendall tau versus Spearman footrule bounds

The lower bound follows by comparing the two diagonal evaluations with the CDF at the sampled point. The upper bound uses C(u,v) <= min(u,v).

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.Support.diagonal_pair_le (C : Copula 2) (u v : ↑unitInterval) : C.cdf ![u, u] + C.cdf ![v, v] ≤ 2 * C.cdf ![u, v] + |↑u - ↑v|

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.Support.tau_footrule_lower (C : Copula 2) : 4 / 3 * C.spearmanFootrule - 1 / 3 ≤ C.kendallTau

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.Support.tau_footrule_upper (C : Copula 2) : C.kendallTau ≤ 2 / 3 * C.spearmanFootrule + 1 / 3