← Copula mathematical handbook

A sharp lower bound for multivariate Spearman's rho: the dual certificate

For a d-copula C (law of U = (U₁, …, U_d)) we have ∫ C dΠ = E[∏ᵢ (1 - Uᵢ)] (integral_cdf_independence_eq_prod), and Xᵢ = -log(1 - Uᵢ) are standard exponential, so minimizing ∫ C dΠ (equivalently the multivariate Spearman's rho ρ_d(C) = (d+1)/(2^d - d - 1) · (2^d ∫ C dΠ - 1)) is the problem of minimizing E[exp(-∑ Xᵢ)] over all dependence structures of d exponential variables. Since the exponential distribution has a decreasing density, the minimal sum in convex order is known (Wang–Wang 2011, Bernard–Jiang–Wang 2014): one large and d - 1 small values on a tail event of probability d c_d, and a joint mix (constant sum) in the middle. This file proves the matching lower bound by an explicit dual certificate; for c = c_d it equals that minimum (see below).

The certificate

Put vᵢ = 1 - Uᵢ ∈ (0, 1], P = ∏ vᵢ, and for 0 < x ≤ 1/(d(d-1))

• q(x) = x (1 - (d-1)x)^{d-1} (level), with derivative q'(x) ≥ 0 (levelDeriv);
• κ_x(v) = max(x, min(v, 1 - (d-1)x)) (clampLevel).

Pointwise inequality (prod_clampLevel_le): ∏ᵢ κ_x(vᵢ) ≤ max(q(x), P): if some vᵢ < x then that factor is x and the others are ≤ 1 - (d-1)x; otherwise κ_x(vᵢ) ≤ vᵢ. Taking logarithms and integrating against q'(x) dx over (0, c], together with ∫₀ᶜ q'(x) max(0, log P - log q(x)) dx ≤ P (integral_levelDeriv_posPart_le), gives the pointwise dual inequality ∑ᵢ ψ_c(vᵢ) - Q_c ≤ P (sum_dualFunction_sub_le_prod) with ψ_c(v) = ∫₀ᶜ q'(x) log κ_x(v) dx and Q_c = ∫₀ᶜ q' log q = q(c) log q(c) - q(c). Integrating against C and using uniform marginals and Fubini (∫₀¹ log κ_x(v) dv = log(1-(d-1)x) + dx - 1) yields the main result:

• dualBound_le_integral_cdf: for d ≥ 2, 0 < c, c d (d-1) ≤ 1 and every d-copula, ∫ C dΠ ≥ L_d(c) := d ∫₀ᶜ q'(x) (log(1 - (d-1)x) + d x - 1) dx - q(c) log q(c) + q(c);
• dualBound_le_multivariateSpearmanRho: the corresponding bound for ρ_d.

Sharpness (not formalized)

Maximizing over c, the optimum c_d solves H(c) = D(c) of Bernard–Jiang–Wang; for d = 3 this is log((1 - 2c)/c) = 3 - 9c, c₃ ≈ 0.0945416, and L₃(c₃) = c₃ - 11c₃²/2 + 12c₃³ - 9c₃⁴ ≈ 0.0548032 (Copula.Multivariate.SpearmanInfimumThree). Numerically L_d(c_d) coincides with E[exp(-T)] for the convex-order minimal sum T of Bernard–Jiang–Wang (2014, Theorem 2.1), which is attained by a copula whose middle part is a joint mix (Wang–Wang 2011, Theorem 2.4), so the bound is the exact infimum: inf ρ₃ ≈ -0.5615741, inf ρ₄ ≈ -0.3156518, inf ρ₅ ≈ -0.1801073. The attainment (existence of the joint mix) is not formalized here.

References: B. Wang and R. Wang, The complete mixability and convex minimization problems with monotone marginal densities, J. Multivariate Anal. 102 (2011) 1344–1360; C. Bernard, X. Jiang and R. Wang, Risk aggregation with dependence uncertainty, Insurance Math. Econom. 54 (2014) 93–108; E. Jakobsons, X. Han and R. Wang, General convex order on risk aggregation, Scand. Actuar. J. 2016, 713–740.

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.level (d : ℕ) (x : ℝ) : ℝ

The tail level q_d(x) = x (1 - (d-1) x)^{d-1}.

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.level d x = x * (1 - (↑d - 1) * x) ^ (d - 1)

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.levelDeriv (d : ℕ) (x : ℝ) : ℝ

The derivative of level: (1 - (d-1)x)^{d-1} - (d-1)² x (1 - (d-1)x)^{d-2}.

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.levelDeriv d x = (1 - (↑d - 1) * x) ^ (d - 1) - (↑d - 1) ^ 2 * x * (1 - (↑d - 1) * x) ^ (d - 2)

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.clampLevel (d : ℕ) (x v : ℝ) : ℝ

The clamp κ_x(v) = max(x, min(v, 1 - (d-1)x)).

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.clampLevel d x v = max x (min v (1 - (↑d - 1) * x))

theorem ProbabilityTheory.Copula.SpearmanInfimum.hasDerivAt_level {d : ℕ} (hd : 2 ≤ d) (x : ℝ) : HasDerivAt (level d) (levelDeriv d x) x

theorem ProbabilityTheory.Copula.SpearmanInfimum.continuous_level (d : ℕ) : Continuous (level d)

theorem ProbabilityTheory.Copula.SpearmanInfimum.le_base {d : ℕ} (hd : 2 ≤ d) {x : ℝ} (hx : 0 ≤ x) (hxd : x * (↑d * (↑d - 1)) ≤ 1) : x ≤ 1 - (↑d - 1) * x

Positivity of the base 1 - (d-1)x and x ≤ 1 - (d-1)x in the admissible range.

theorem ProbabilityTheory.Copula.SpearmanInfimum.levelDeriv_nonneg {d : ℕ} (hd : 2 ≤ d) {x : ℝ} (hx : 0 ≤ x) (hxd : x * (↑d * (↑d - 1)) ≤ 1) : 0 ≤ levelDeriv d x

theorem ProbabilityTheory.Copula.SpearmanInfimum.level_pos {d : ℕ} (hd : 2 ≤ d) {x : ℝ} (hx : 0 < x) (hxd : x * (↑d * (↑d - 1)) ≤ 1) : 0 < level d x

theorem ProbabilityTheory.Copula.SpearmanInfimum.level_zero {d : ℕ} : level d 0 = 0

theorem ProbabilityTheory.Copula.SpearmanInfimum.monotoneOn_level {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc : c * (↑d * (↑d - 1)) ≤ 1) : MonotoneOn (level d) (Set.Icc 0 c)

level is monotone on the admissible range [0, c].

The pointwise inequality

theorem ProbabilityTheory.Copula.SpearmanInfimum.clampLevel_nonneg {d : ℕ} {x v : ℝ} (hx : 0 ≤ x) : 0 ≤ clampLevel d x v

theorem ProbabilityTheory.Copula.SpearmanInfimum.clampLevel_le_base {d : ℕ} {x v : ℝ} (hb : x ≤ 1 - (↑d - 1) * x) : clampLevel d x v ≤ 1 - (↑d - 1) * x

theorem ProbabilityTheory.Copula.SpearmanInfimum.prod_clampLevel_le {d : ℕ} {x : ℝ} (hx : 0 ≤ x) (hb : x ≤ 1 - (↑d - 1) * x) (v : Fin d → ℝ) : ∏ i : Fin d, clampLevel d x (v i) ≤ max (level d x) (∏ i : Fin d, v i)

The pointwise inequality: ∏ᵢ κ_x(vᵢ) ≤ max(q(x), ∏ᵢ vᵢ).

theorem ProbabilityTheory.Copula.SpearmanInfimum.sum_log_clampLevel_sub_le {d : ℕ} (hd : 2 ≤ d) {x : ℝ} (hx : 0 < x) (hxd : x * (↑d * (↑d - 1)) ≤ 1) {v : Fin d → ℝ} (hv : ∀ (i : Fin d), 0 < v i) : ∑ i : Fin d, Real.log (clampLevel d x (v i)) - Real.log (level d x) ≤ max 0 (Real.log (∏ i : Fin d, v i) - Real.log (level d x))

Logarithmic form of the pointwise inequality.

The integral of the positive part

theorem ProbabilityTheory.Copula.SpearmanInfimum.continuous_levelDeriv (d : ℕ) : Continuous (levelDeriv d)

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurable_clampLevel (d : ℕ) : Measurable fun (p : ℝ × ℝ) => clampLevel d p.1 p.2

Integrability

theorem ProbabilityTheory.Copula.SpearmanInfimum.intervalIntegrable_log_level {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : IntervalIntegrable (fun (x : ℝ) => Real.log (level d x)) MeasureTheory.volume 0 c

log ∘ q is interval integrable on [0, c].

theorem ProbabilityTheory.Copula.SpearmanInfimum.intervalIntegrable_levelDeriv_mul_log_level {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : IntervalIntegrable (fun (x : ℝ) => levelDeriv d x * Real.log (level d x)) MeasureTheory.volume 0 c

theorem ProbabilityTheory.Copula.SpearmanInfimum.intervalIntegrable_levelDeriv_mul_log_clamp {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) (v : ℝ) : IntervalIntegrable (fun (x : ℝ) => levelDeriv d x * Real.log (clampLevel d x v)) MeasureTheory.volume 0 c

x ↦ q'(x) log κ_x(v) is interval integrable on [0, c].

The integral of the positive part

theorem ProbabilityTheory.Copula.SpearmanInfimum.intervalIntegrable_posPart {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) (P : ℝ) : IntervalIntegrable (fun (x : ℝ) => levelDeriv d x * max 0 (Real.log P - Real.log (level d x))) MeasureTheory.volume 0 c

Interval integrability of x ↦ q'(x) max(0, log P - log q(x)) on [0, c].

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_levelDeriv_posPart_le {d : ℕ} (hd : 2 ≤ d) {c P : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) (hP : 0 < P) : ∫ (x : ℝ) in 0..c, levelDeriv d x * max 0 (Real.log P - Real.log (level d x)) ≤ P

∫₀ᶜ q'(x) max(0, log P - log q(x)) dx ≤ P for P > 0.

The dual function and the pointwise dual inequality

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.dualFunction (d : ℕ) (c v : ℝ) : ℝ

The dual function ψ_c(v) = ∫₀ᶜ q'(x) log κ_x(v) dx.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.dualConstant (d : ℕ) (c : ℝ) : ℝ

The dual constant Q_c = ∫₀ᶜ q'(x) log q(x) dx.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.SpearmanInfimum.dualConstant_eq {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : dualConstant d c = level d c * Real.log (level d c) - level d c

Q_c = q(c) log q(c) - q(c).

theorem ProbabilityTheory.Copula.SpearmanInfimum.sum_dualFunction_sub_le_prod {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) {v : Fin d → ℝ} (hv0 : ∀ (i : Fin d), 0 < v i) : ∑ i : Fin d, dualFunction d c (v i) - dualConstant d c ≤ ∏ i : Fin d, v i

The pointwise dual inequality: for vᵢ > 0, ∑ᵢ ψ_c(vᵢ) - Q_c ≤ ∏ᵢ vᵢ.

theorem ProbabilityTheory.Copula.SpearmanInfimum.monotone_dualFunction {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : Monotone (dualFunction d c)

ψ_c is monotone.

Integrating the dual inequality against a copula

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurable_dualFunction_symm {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : Measurable fun (t : ↑unitInterval) => dualFunction d c (1 - ↑t)

theorem ProbabilityTheory.Copula.SpearmanInfimum.integrable_dualFunction_symm {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : MeasureTheory.Integrable (fun (t : ↑unitInterval) => dualFunction d c (1 - ↑t)) MeasureTheory.volume

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_dualFunction_sub_le {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) (C : Copula d) : (↑d * ∫ (t : ↑unitInterval), dualFunction d c (1 - ↑t)) - dualConstant d c ≤ ∫ (u : Fin d → ↑unitInterval), C.cdf u ∂(independence d).toMeasure

Integrating the pointwise dual inequality against a copula: d ∫₀¹ ψ_c(1 - t) dt - Q_c ≤ ∫ C dΠ.

Fubini: the integral of the dual function

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_log_clampLevel {d : ℕ} (hd : 2 ≤ d) {x : ℝ} (hx : 0 < x) (hxd : x * (↑d * (↑d - 1)) ≤ 1) : ∫ (v : ℝ) in 0..1, Real.log (clampLevel d x v) = Real.log (1 - (↑d - 1) * x) + ↑d * x - 1

∫₀¹ log κ_x(v) dv = log(1 - (d-1)x) + d x - 1.

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_dualFunction_symm {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) : ∫ (t : ↑unitInterval), dualFunction d c (1 - ↑t) = ∫ (x : ℝ) in 0..c, levelDeriv d x * (Real.log (1 - (↑d - 1) * x) + ↑d * x - 1)

Fubini: ∫₀¹ ψ_c(1 - t) dt = ∫₀ᶜ q'(x) (log(1 - (d-1)x) + d x - 1) dx.

The main result

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.dualBound (d : ℕ) (c : ℝ) : ℝ

The dual lower bound L_d(c) = d ∫₀ᶜ q'(x) (log(1 - (d-1)x) + d x - 1) dx - q(c) log q(c) + q(c).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.SpearmanInfimum.dualBound_le_integral_cdf {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) (C : Copula d) : dualBound d c ≤ ∫ (u : Fin d → ↑unitInterval), C.cdf u ∂(independence d).toMeasure

The dual lower bound for ∫ C dΠ: for d ≥ 2, 0 ≤ c ≤ 1/(d(d-1)) and every d-copula, L_d(c) ≤ ∫ C dΠ. For c = c_d (the Bernard–Jiang–Wang threshold) this is the exact infimum.

theorem ProbabilityTheory.Copula.dualBound_le_multivariateSpearmanRho {d : ℕ} (hd : 2 ≤ d) {c : ℝ} (hc0 : 0 ≤ c) (hc : c * (↑d * (↑d - 1)) ≤ 1) (C : Copula d) : (↑d + 1) / (2 ^ d - ↑d - 1) * (2 ^ d * SpearmanInfimum.dualBound d c - 1) ≤ C.multivariateSpearmanRho

The dual lower bound for multivariate Spearman's rho: ρ_d(C) ≥ (d+1)/(2^d - d - 1) · (2^d L_d(c) - 1) for d ≥ 2, 0 ≤ c ≤ 1/(d(d-1)).