← Copula mathematical handbook

The lower bound of multivariate Spearman's rho is not best possible for d ≥ 3

Copula.Multivariate.SpearmanLowerBound proves the classical bound ρ_d(C) ≥ (2^d - (d+1)!) / (d! (2^d - d - 1)) for the multivariate Spearman's rho ρ_d(C) = (d+1)/(2^d - d - 1) · (2^d ∫ C dΠ - 1) (Nelsen 1996; Schmid–Schmidt 2007, ρ₁), which comes from C ≥ W_d and ∫ W_d dΠ = 1/(d+1)!. For d = 2 it is the sharp bound -1. For d ≥ 3 the lower Fréchet–Hoeffding bound W_d is not a copula, and the bound is in fact not best possible: there is a uniform gap.

Main results:

• exp_neg_le_integral_cdf: ∫ C dΠ ≥ e^{-d} for every d-copula. Proof: by Fubini ∫ C dΠ = E_C[∏ᵢ (1 - Uᵢ)] = E_C[exp(∑ᵢ log(1 - Uᵢ))]; the tangent line exp(s) ≥ e^{-d} (1 + d + s) and E[log(1 - Uᵢ)] = ∫₀¹ log(1 - t) dt = -1 give ∫ C dΠ ≥ e^{-d} (this is Jensen's inequality for exp).
• exp_lt_factorial: e^d < (d+1)! for d ≥ 3, hence 1/(d+1)! < e^{-d}.
• one_div_factorial_lt_integral_cdf: for d ≥ 3, ∫ C dΠ > 1/(d+1)! for every copula (so the bound is never attained), and le_multivariateSpearmanRho_exp: ρ_d(C) ≥ (d+1)/(2^d - d - 1) · (2^d e^{-d} - 1), which is strictly larger than the classical bound for d ≥ 3 (lowerBound_lt_expBound).
• exists_gap_multivariateSpearmanRho: for d ≥ 3 there is ε > 0 with ρ_d(C) ≥ (2^d - (d+1)!)/(d!(2^d - d - 1)) + ε for all C; in particular the classical bound is not the infimum (not_isGLB_lowerBound). For d = 3: ρ₃(C) ≥ 8e^{-3} - 1 ≈ -0.6017 > -2/3 (multivariateSpearmanRho_three_ge).

The exact infimum is not determined here. The bound 8e^{-3} - 1 ≈ -0.6017 is not attained, since -log(1 - Uᵢ) are exponential and cannot have a constant sum. The sharp dual bound (Copula.Multivariate.SpearmanInfimumDual) gives ρ₃ ≥ -0.56158 (Copula.Multivariate.SpearmanInfimumThree), and an explicit copula has ρ₃ = -631/1125 (Copula.Multivariate.SpearmanInfimumWitness); numerically the infimum is ≈ -0.5615741.

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.

theorem ProbabilityTheory.Copula.integrable_log_one_sub : MeasureTheory.Integrable (fun (t : ↑unitInterval) => Real.log (1 - ↑t)) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integral_log_one_sub : ∫ (t : ↑unitInterval), Real.log (1 - ↑t) = -1

∫₀¹ log(1 - t) dt = -1.

theorem ProbabilityTheory.Copula.integrable_log_one_sub_eval {d : ℕ} (C : Copula d) (i : Fin d) : MeasureTheory.Integrable (fun (y : Fin d → ↑unitInterval) => Real.log (1 - ↑(y i))) C.toMeasure

theorem ProbabilityTheory.Copula.integral_log_one_sub_eval {d : ℕ} (C : Copula d) (i : Fin d) : ∫ (y : Fin d → ↑unitInterval), Real.log (1 - ↑(y i)) ∂C.toMeasure = -1

theorem ProbabilityTheory.Copula.exp_neg_mul_le_prod {d : ℕ} {y : Fin d → ↑unitInterval} (hy : ∀ (i : Fin d), ↑(y i) < 1) : Real.exp (-↑d) * (1 + ↑d + ∑ i : Fin d, Real.log (1 - ↑(y i))) ≤ ∏ i : Fin d, (1 - ↑(y i))

The tangent-line inequality behind Jensen's bound: for yᵢ < 1, ∏ᵢ (1 - yᵢ) ≥ e^{-d} (1 + d + ∑ᵢ log(1 - yᵢ)).

theorem ProbabilityTheory.Copula.exp_neg_le_integral_cdf {d : ℕ} (C : Copula d) : Real.exp (-↑d) ≤ ∫ (u : Fin d → ↑unitInterval), C.cdf u ∂(independence d).toMeasure

Jensen's lower bound: every d-copula satisfies ∫ C dΠ ≥ e^{-d}.

theorem ProbabilityTheory.Copula.exp_lt_factorial {d : ℕ} (hd : 3 ≤ d) : Real.exp ↑d < ↑(d + 1).factorial

e^d < (d+1)! for d ≥ 3.

theorem ProbabilityTheory.Copula.one_div_factorial_lt_exp_neg {d : ℕ} (hd : 3 ≤ d) : 1 / ↑(d + 1).factorial < Real.exp (-↑d)

1/(d+1)! < e^{-d} for d ≥ 3.

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

For d ≥ 3 the bound ∫ C dΠ ≥ 1/(d+1)! is strict for every copula: it is never attained (W_d is not a copula).

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

Improved lower bound of multivariate Spearman's rho: ρ_d(C) ≥ (d+1)/(2^d - d - 1) · (2^d e^{-d} - 1) for every d-copula, d ≥ 2.

theorem ProbabilityTheory.Copula.lowerBound_lt_expBound {d : ℕ} (hd : 3 ≤ d) : (2 ^ d - ↑(d + 1).factorial) / (↑d.factorial * (2 ^ d - ↑d - 1)) < (↑d + 1) / (2 ^ d - ↑d - 1) * (2 ^ d * Real.exp (-↑d) - 1)

For d ≥ 3 the improved bound is strictly larger than the classical bound (2^d - (d+1)!)/(d!(2^d - d - 1)).

theorem ProbabilityTheory.Copula.exists_gap_multivariateSpearmanRho {d : ℕ} (hd : 3 ≤ d) : ∃ ε > 0, ∀ (C : Copula d), (2 ^ d - ↑(d + 1).factorial) / (↑d.factorial * (2 ^ d - ↑d - 1)) + ε ≤ C.multivariateSpearmanRho

The classical lower bound is not best possible for d ≥ 3: there is a uniform gap ε > 0 with ρ_d(C) ≥ (2^d - (d+1)!)/(d!(2^d - d - 1)) + ε for every d-copula.

theorem ProbabilityTheory.Copula.not_isGLB_lowerBound {d : ℕ} (hd : 3 ≤ d) : ¬IsGLB (Set.range fun (C : Copula d) => C.multivariateSpearmanRho) ((2 ^ d - ↑(d + 1).factorial) / (↑d.factorial * (2 ^ d - ↑d - 1)))

For d ≥ 3 the classical lower bound is not the infimum of ρ_d over d-copulas.

theorem ProbabilityTheory.Copula.multivariateSpearmanRho_three_ge (C : Copula 3) : 8 * Real.exp (-3) - 1 ≤ C.multivariateSpearmanRho

For d = 3: ρ₃(C) ≥ 8e^{-3} - 1 ≈ -0.6017, strictly above the classical bound -2/3.

theorem ProbabilityTheory.Copula.neg_two_thirds_lt_exp_bound_three : -2 / 3 < 8 * Real.exp (-3) - 1