← Copula mathematical handbook

The lower bound of trivariate Spearman's rho in closed form

For d = 3 the dual bound of Copula.Multivariate.SpearmanInfimumDual has the closed form

L₃(c) = c (1 - 2c)² log((1 - 2c)/c) - 2c + 31c²/2 - 36c³ + 27c⁴ (dualBound_three),

valid for 0 < c ≤ 1/6, so that ∫ C dΠ ≥ L₃(c) and ρ₃(C) = 8 ∫ C dΠ - 1 ≥ 8 L₃(c) - 1 for every 3-copula (dualBoundThree_le_integral_cdf, le_multivariateSpearmanRho_three).

• The optimal parameter solves log((1 - 2c)/c) = 3 - 9c (the stationarity condition of L₃, equivalently Bernard–Jiang–Wang's H(c) = D(c) for the exponential distribution). Such a root c₃ ∈ (1/12, 1/6) exists (exists_optimal_parameter), and there the bound is the polynomial m₃ = c₃ - 11c₃²/2 + 12c₃³ - 9c₃⁴ (dualBoundThree_eq_of_optimal, le_multivariateSpearmanRho_three_optimal). Numerically c₃ ≈ 0.0945415778, m₃ ≈ 0.0548032411 and 8m₃ - 1 ≈ -0.5615740714.
• A certified numerical consequence (neg_056158_le_multivariateSpearmanRho_three): ρ₃(C) ≥ -0.56158 for every 3-copula, from c = 7/74 and log(60/7) > 2.14843.

Together with the explicit copula of Copula.Multivariate.SpearmanInfimumWitness (ρ₃ = -631/1125 ≈ -0.560889) this pins the infimum of ρ₃ to [-0.56158, -0.560888]; by the convex-order theory of Wang–Wang (2011) and Bernard–Jiang–Wang (2014) the infimum is 8m₃ - 1 and is attained (not formalized).

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.dualBoundThree (c : ℝ) : ℝ

The closed form L₃(c) = c (1-2c)² log((1-2c)/c) - 2c + 31c²/2 - 36c³ + 27c⁴.

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.dualBoundThree c = c * (1 - 2 * c) ^ 2 * Real.log ((1 - 2 * c) / c) - 2 * c + 31 / 2 * c ^ 2 - 36 * c ^ 3 + 27 * c ^ 4

theorem ProbabilityTheory.Copula.SpearmanInfimum.dualBound_three {c : ℝ} (hc0 : 0 < c) (hc : c ≤ 1 / 6) : dualBound 3 c = dualBoundThree c

Closed form of the dual bound for d = 3: dualBound 3 c = L₃(c) for 0 < c ≤ 1/6.

theorem ProbabilityTheory.Copula.SpearmanInfimum.dualBoundThree_le_integral_cdf {c : ℝ} (hc0 : 0 < c) (hc : c ≤ 1 / 6) (C : Copula 3) : dualBoundThree c ≤ ∫ (u : Fin 3 → ↑unitInterval), C.cdf u ∂(independence 3).toMeasure

The dual lower bound for d = 3: ∫ C dΠ ≥ L₃(c) for 0 < c ≤ 1/6.

theorem ProbabilityTheory.Copula.SpearmanInfimum.multivariateSpearmanRho_three_eq (C : Copula 3) : C.multivariateSpearmanRho = 8 * ∫ (u : Fin 3 → ↑unitInterval), C.cdf u ∂(independence 3).toMeasure - 1

ρ₃(C) = 8 ∫ C dΠ - 1.

theorem ProbabilityTheory.Copula.SpearmanInfimum.dualBoundThree_eq_of_optimal {c : ℝ} (h : Real.log ((1 - 2 * c) / c) = 3 - 9 * c) : dualBoundThree c = c - 11 / 2 * c ^ 2 + 12 * c ^ 3 - 9 * c ^ 4

L₃ at a root of the stationarity equation log((1 - 2c)/c) = 3 - 9c.

theorem ProbabilityTheory.Copula.SpearmanInfimum.exists_optimal_parameter : ∃ c ∈ Set.Ioo (1 / 12) (1 / 6), Real.log ((1 - 2 * c) / c) = 3 - 9 * c

The optimal parameter exists: some c₃ ∈ (1/12, 1/6) solves log((1 - 2c)/c) = 3 - 9c.

theorem ProbabilityTheory.Copula.SpearmanInfimum.le_multivariateSpearmanRho_three_optimal {c : ℝ} (hc0 : 0 < c) (hc : c ≤ 1 / 6) (hopt : Real.log ((1 - 2 * c) / c) = 3 - 9 * c) (C : Copula 3) : 8 * (c - 11 / 2 * c ^ 2 + 12 * c ^ 3 - 9 * c ^ 4) - 1 ≤ C.multivariateSpearmanRho

The optimal dual bound: with c₃ a root of log((1-2c)/c) = 3 - 9c in (0, 1/6], ρ₃(C) ≥ 8 (c₃ - 11c₃²/2 + 12c₃³ - 9c₃⁴) - 1 ≈ -0.5615741 for every 3-copula.

theorem ProbabilityTheory.Copula.SpearmanInfimum.le_multivariateSpearmanRho_three {c : ℝ} (hc0 : 0 < c) (hc : c ≤ 1 / 6) (C : Copula 3) : 8 * dualBoundThree c - 1 ≤ C.multivariateSpearmanRho

The bound ρ₃(C) ≥ 8 L₃(c) - 1 for 0 < c ≤ 1/6.

theorem ProbabilityTheory.Copula.SpearmanInfimum.neg_056158_le_multivariateSpearmanRho_three (C : Copula 3) : -0.56158 ≤ C.multivariateSpearmanRho

Certified numerical lower bound: ρ₃(C) ≥ -0.56158 for every 3-copula (from c = 7/74). The exact infimum is ≈ -0.5615741; in particular no 3-copula has ρ₃ ≤ -0.5616.