← Mathematical handbook

Complementary slackness for the rho--footrule dual

theorem Verification.dual_contact_of_cost_eq (C : ProbabilityTheory.Copula 2) (g : ℝ → ℝ) (θ : ℝ) (hg : Continuous g) (hf : ∀ (a b : ℝ), g a + g b ≤ (b - a) ^ 2 - θ * |b - a|) (he : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂C.toMeasure - θ * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure = 2 * ∫ (u : ↑unitInterval), g ↑u) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, g ↑(x 0) + g ↑(x 1) = (↑(x 1) - ↑(x 0)) ^ 2 - θ * |↑(x 1) - ↑(x 0)|

An attained dual cost forces equality in the dual constraint almost everywhere.

theorem Verification.dual_ranks_unique (C D : ProbabilityTheory.Copula 2) (g : ℝ → ℝ) (v : NNReal) (θ : ℝ) (hg : LipschitzWith v g) (hθ : ↑v < θ) (hf : ∀ (a b : ℝ), g a + g b ≤ (b - a) ^ 2 - θ * |b - a|) (he : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂D.toMeasure - θ * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂D.toMeasure = 2 * ∫ (u : ↑unitInterval), g ↑u) (hp : C.spearmanFootrule = D.spearmanFootrule) (hr : C.spearmanRho = D.spearmanRho) : C = D

An attained strictly Lipschitz dual identifies every copula with the same two ranks.