← Copula mathematical handbook

Daniels' inequality between Kendall's tau and Spearman's rho

Daniels (1950) proved -1 ≤ 3τ - 2ρ ≤ 1 for every continuous bivariate distribution (Nelsen, An Introduction to Copulas, 2nd ed., §5.1.3). We derive it from the exact (τ, ρ) region of Schreyer, Paulin and Trutschnig (2017), formalized in Copula.Rank.Region.RhoTau: every copula lies above a point of the lower boundary with the same τ and below the reflection of a boundary point with opposite τ, and along each polynomial boundary arc

1 - (3 τ - 2 ρ) = 2 n ((n+1)³ - 3 (n+1) s² - 2 s³) / ((n+1)² (n+2)²) ≥ 0.

The bound is attained, e.g. at (τ, ρ) = (0, -1/2) (the arc n = 1, s = 1).

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.three_mul_tau_sub_two_mul_rho_le (p : LowerParameter) : 3 * p.tau - 2 * p.rho ≤ 1

Daniels' bound at every lower boundary parameter.

theorem ProbabilityTheory.Copula.three_mul_kendallTau_sub_two_mul_spearmanRho_le (C : Copula 2) : 3 * C.kendallTau - 2 * C.spearmanRho ≤ 1

Daniels' inequality, upper half: 3 τ - 2 ρ ≤ 1 (Nelsen, §5.1.3).

theorem ProbabilityTheory.Copula.neg_one_le_three_mul_kendallTau_sub_two_mul_spearmanRho (C : Copula 2) : -1 ≤ 3 * C.kendallTau - 2 * C.spearmanRho

Daniels' inequality, lower half: -1 ≤ 3 τ - 2 ρ (Nelsen, §5.1.3).

theorem ProbabilityTheory.Copula.abs_three_mul_kendallTau_sub_two_mul_spearmanRho_le (C : Copula 2) : |3 * C.kendallTau - 2 * C.spearmanRho| ≤ 1

Daniels' inequality |3 τ - 2 ρ| ≤ 1 (Daniels 1950; Nelsen, §5.1.3).