← Mathematical handbook

Uniqueness of copulas saturating a strictly Lipschitz distance dual

noncomputable def Verification.dualForward (g : ℝ → ℝ) (θ : ℝ) (a : ↑unitInterval) : ↑unitInterval

Equations

• Verification.dualForward g θ a = Set.projIcc 0 1 Verification.dualForward._proof_1 (↑a + (θ - deriv g ↑a) / 2)

theorem Verification.measurable_dualForward (g : ℝ → ℝ) (θ : ℝ) : Measurable (dualForward g θ)

theorem Verification.dual_contact_graph_support (C : ProbabilityTheory.Copula 2) (g : ℝ → ℝ) (v : NNReal) (θ : ℝ) (hg : LipschitzWith v g) (hθ : ↑v < θ) (hf : ∀ (a b : ℝ), g a + g b ≤ (b - a) ^ 2 - θ * |b - a|) (hC : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, g ↑(x 0) + g ↑(x 1) = (↑(x 1) - ↑(x 0)) ^ 2 - θ * |↑(x 1) - ↑(x 0)|) : ForwardGraphSupport C (dualForward g θ) ((θ - ↑v) / 2)

Equality in the distance dual forces support on one forward graph and its transpose.

theorem Verification.copula_dual_contact_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|) (hC : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, g ↑(x 0) + g ↑(x 1) = (↑(x 1) - ↑(x 0)) ^ 2 - θ * |↑(x 1) - ↑(x 0)|) (hD : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, g ↑(x 0) + g ↑(x 1) = (↑(x 1) - ↑(x 0)) ^ 2 - θ * |↑(x 1) - ↑(x 0)|) : C = D

The global dual inequality and a strict Lipschitz gap imply uniqueness, even among nonsymmetric copulas and singular measures.