← 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 Verification.diagonal_pair_le (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : C.cdf ![u, u] + C.cdf ![v, v] ≤ 2 * C.cdf ![u, v] + |↑u - ↑v|

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

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