← Copula mathematical handbook

Multivariate Kendall's tau and Spearman's rho

For a d-copula C (d ≥ 2) the multivariate versions of Kendall's tau and of Spearman's rho (Joe 1990, "Multivariate concordance", J. Multivariate Anal. 35; Nelsen 1996, "Nonparametric measures of multivariate association"; Schmid–Schmidt 2007, ρ₁) are

• τ_d(C) = (2^d ∫ C dC - 1) / (2^{d-1} - 1) (multivariateKendallTau),
• ρ_d(C) = (d + 1) / (2^d - d - 1) · (2^d ∫ C dΠ - 1) (multivariateSpearmanRho).

We prove:

• for d = 2 they are Kendall's tau and Spearman's rho (multivariateKendallTau_two, multivariateSpearmanRho_two);
• the Fubini identity ∫ C dΠ = ∫ ∏ (1 - xᵢ) dC(x) (integral_cdf_independence_eq_prod);
• both vanish at Π_d and equal 1 at M_d (multivariateKendallTau_independence, multivariateKendallTau_comonotonic, multivariateSpearmanRho_independence, multivariateSpearmanRho_comonotonic);
• the bounds -1/(2^{d-1} - 1) ≤ τ_d ≤ 1 and ρ_d ≤ 1, and monotonicity of ρ_d in the lower-orthant order (multivariateSpearmanRho_mono).

noncomputable def ProbabilityTheory.Copula.multivariateKendallTau {d : ℕ} (C : Copula d) : ℝ

Multivariate Kendall's tau τ_d(C) = (2^d ∫ C dC - 1) / (2^{d-1} - 1) (Joe 1990).

Equations

• C.multivariateKendallTau = (2 ^ d * ∫ (x : Fin d → ↑unitInterval), C.cdf x ∂C.toMeasure - 1) / (2 ^ (d - 1) - 1)

noncomputable def ProbabilityTheory.Copula.multivariateSpearmanRho {d : ℕ} (C : Copula d) : ℝ

Multivariate Spearman's rho ρ_d(C) = (d+1)/(2^d - d - 1) · (2^d ∫ C dΠ - 1) (Joe 1990; Schmid–Schmidt 2007).

Equations

• C.multivariateSpearmanRho = (↑d + 1) / (2 ^ d - ↑d - 1) * (2 ^ d * ∫ (x : Fin d → ↑unitInterval), C.cdf x ∂(ProbabilityTheory.Copula.independence d).toMeasure - 1)

theorem ProbabilityTheory.Copula.dim_add_one_lt_two_pow {d : ℕ} (hd : 2 ≤ d) : ↑d + 1 < 2 ^ d

2^d > d + 1 for d ≥ 2.

Dimension two

theorem ProbabilityTheory.Copula.multivariateKendallTau_two (C : Copula 2) : C.multivariateKendallTau = C.kendallTau

theorem ProbabilityTheory.Copula.multivariateSpearmanRho_two (C : Copula 2) : C.multivariateSpearmanRho = C.spearmanRho

A Fubini identity

theorem ProbabilityTheory.Copula.integral_cdf_independence_eq_prod {d : ℕ} (C : Copula d) : ∫ (x : Fin d → ↑unitInterval), C.cdf x ∂(independence d).toMeasure = ∫ (y : Fin d → ↑unitInterval), ∏ i : Fin d, (1 - ↑(y i)) ∂C.toMeasure

∫ C dΠ = ∫ ∏ (1 - xᵢ) dC(x): both are P(X ≤ V) for X ∼ C independent of a uniform vector V.

Benchmarks

theorem ProbabilityTheory.Copula.multivariateKendallTau_independence {d : ℕ} : (independence d).multivariateKendallTau = 0

theorem ProbabilityTheory.Copula.multivariateSpearmanRho_independence {d : ℕ} : (independence d).multivariateSpearmanRho = 0

theorem ProbabilityTheory.Copula.multivariateKendallTau_comonotonic {d : ℕ} (hd : 2 ≤ d) : (comonotonic d).multivariateKendallTau = 1

theorem ProbabilityTheory.Copula.multivariateSpearmanRho_comonotonic {d : ℕ} (hd : 2 ≤ d) : (comonotonic d).multivariateSpearmanRho = 1

Bounds and monotonicity

theorem ProbabilityTheory.Copula.multivariateSpearmanRho_mono {d : ℕ} (hd : 2 ≤ d) {C D : Copula d} (h : C.LowerOrthantLE D) : C.multivariateSpearmanRho ≤ D.multivariateSpearmanRho

ρ_d is nondecreasing in the lower-orthant order.

theorem ProbabilityTheory.Copula.multivariateSpearmanRho_le_one {d : ℕ} (hd : 2 ≤ d) (C : Copula d) : C.multivariateSpearmanRho ≤ 1

ρ_d ≤ 1, with equality at M_d.

theorem ProbabilityTheory.Copula.multivariateKendallTau_le_one {d : ℕ} (hd : 2 ≤ d) (C : Copula d) : C.multivariateKendallTau ≤ 1

τ_d ≤ 1, with equality at M_d.

theorem ProbabilityTheory.Copula.neg_inv_le_multivariateKendallTau {d : ℕ} (hd : 2 ≤ d) (C : Copula d) : -1 / (2 ^ (d - 1) - 1) ≤ C.multivariateKendallTau

τ_d ≥ -1/(2^{d-1} - 1), the trivial lower bound (sharp for d = 2).