← Copula mathematical handbook

The lower bound of multivariate Spearman's rho

The lower Fréchet–Hoeffding bound W_d(u) = max(0, u₁ + ⋯ + u_d - d + 1) satisfies

∫_{[0,1]^d} W_d dΠ_d = 1 / (d+1)!

(integral_lowerFrechetBound): after the reflection vᵢ = 1 - uᵢ it is the integral of max(0, 1 - ∑ vᵢ) over the cube, i.e. the volume of the (d+1)-dimensional simplex. Since every d-copula dominates W_d pointwise, ∫ C dΠ ≥ 1/(d+1)!, and the multivariate Spearman's rho ρ_d(C) = (d+1)/(2^d - d - 1) · (2^d ∫ C dΠ - 1) (multivariateSpearmanRho) satisfies

ρ_d(C) ≥ (2^d - (d+1)!) / (d! (2^d - d - 1))

(le_multivariateSpearmanRho; Nelsen 1996, Joe 1990; Schmid–Schmidt 2007). For d = 2 this is -1 (attained at W), for d = 3 it is -2/3.

The integral is computed by induction on the dimension: for s ≤ 1, ∫_{[0,1]^n} max(0, s - ∑(1 - xᵢ)) dx = max(0, s)^{n+1} / (n+1)! (integral_max_zero_sub_sum).

References: R. B. Nelsen, Nonparametric measures of multivariate association (1996); F. Schmid and R. Schmidt, Multivariate extensions of Spearman's rho and related statistics, Statist. Probab. Lett. 77 (2007) 407–416; H. Joe, Multivariate concordance, J. Multivariate Anal. 35 (1990).

theorem ProbabilityTheory.Copula.integral_unit_max_zero_pow (k : ℕ) {s : ℝ} (hs : s ≤ 1) : ∫ (t : ↑unitInterval), max 0 (s - (1 - ↑t)) ^ (k + 1) = max 0 s ^ (k + 2) / (↑k + 2)

∫₀¹ max(0, s - (1 - t))^{k+1} dt = max(0, s)^{k+2} / (k+2) for s ≤ 1.

theorem ProbabilityTheory.Copula.integral_max_zero_sub_sum (n : ℕ) {s : ℝ} (hs : s ≤ 1) : (∫ (x : Fin n → ↑unitInterval), max 0 (s - ∑ i : Fin n, (1 - ↑(x i))) ∂MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.volume) = max 0 s ^ (n + 1) / ↑(n + 1).factorial

Volume of the simplex: for s ≤ 1, ∫_{[0,1]^n} max(0, s - ∑ (1 - xᵢ)) dx = max(0, s)^{n+1} / (n+1)!.

theorem ProbabilityTheory.Copula.integral_lowerFrechetBound (d : ℕ) : ∫ (u : Fin d → ↑unitInterval), lowerFrechetBound d u ∂(independence d).toMeasure = 1 / ↑(d + 1).factorial

∫ W_d dΠ_d = 1/(d+1)!.

theorem ProbabilityTheory.Copula.one_div_factorial_le_integral_cdf {d : ℕ} (C : Copula d) : 1 / ↑(d + 1).factorial ≤ ∫ (u : Fin d → ↑unitInterval), C.cdf u ∂(independence d).toMeasure

Every d-copula has ∫ C dΠ ≥ 1/(d+1)!.

theorem ProbabilityTheory.Copula.le_multivariateSpearmanRho {d : ℕ} (hd : 2 ≤ d) (C : Copula d) : (2 ^ d - ↑(d + 1).factorial) / (↑d.factorial * (2 ^ d - ↑d - 1)) ≤ C.multivariateSpearmanRho

Lower bound of multivariate Spearman's rho: ρ_d(C) ≥ (2^d - (d+1)!) / (d! (2^d - d - 1)) for every d-copula, d ≥ 2 (Nelsen 1996; Schmid–Schmidt 2007).

theorem ProbabilityTheory.Copula.neg_two_thirds_le_multivariateSpearmanRho_three (C : Copula 3) : -2 / 3 ≤ C.multivariateSpearmanRho

For d = 3 the lower bound is ρ₃ ≥ -2/3.