Theorem 1 — strong duality , a dual optimizer and complementary slackness
OpenModelRiskOT.Duality.theorem_1Let be a Polish space, a Borel probability measure on , a lower semicontinuous cost with if and only if (Assumption (A1)), upper semicontinuous and -integrable (Assumption (A2)), and . Let be the worst-case expectation of over transport plans out of with cost at most , and its dual. For let . Then:
- (a) Strong duality.
- (b) Dual attainment. There is such that and .
- (b) Complementary slackness, "if". For and , if
then is a primal optimizer (), is a dual optimizer (), and . 4. (b) Complementary slackness, "only if". Conversely, if and are as in 3., are primal and dual optimizers with , and , then (8a) and (8b) hold.
Theorem 1 says that the worst-case expectation over an optimal-transport ball on a general Polish space, with only lower semicontinuous costs and upper semicontinuous integrable , equals a one-dimensional dual problem over , and it characterizes worst-case transport plans.
Formalization Note The finiteness hypothesis in item 4 is implicit in the paper: when outgrows on a set of positive -measure, there, , and an optimal with can exist while (8a) is impossible ( is finite). The direction "if" holds without it. By weak duality, "primal and dual optimizers satisfying " is equivalent to alone; the statement spells out all three equalities. In (8b) the cost integral is converted to a real number, which is safe because it is at most . The space is a Polish space with its Borel σ-algebra; the cost is real-valued and written curried, ; (A1) is the structure AssumptionA1; (A2) is the pair of hypotheses UpperSemicontinuous f and Integrable f μ. Values that can be infinite (, , , , ) live in EReal; an integral of an extended-real function is with lower Lebesgue integrals, and evaluates to , so a coupling with never raises the primal supremum (the paper's footnote 2 reading).
import Mathlib import Definitions.Def_ModelRiskOT_Duality_AssumptionA1 import Definitions.Def_ModelRiskOT_Duality_primalValue import Definitions.Def_ModelRiskOT_Duality_dualValue import Definitions.Def_ModelRiskOT_Duality_phiLam open MeasureTheory
namespace ModelRiskOT.Duality
/-- **Theorem 1** (Blanchet & Murthy, arXiv:1604.01446v2, p. 7). Under (A1) and (A2), with `δ > 0`:
1. (a) strong duality `I = J`;
2. (b) a dual optimizer of the form `(λ, φ_λ)`, `λ ≥ 0`, exists;
3. (b, "if") for `π* ∈ Φ_{μ,δ}` and `(λ*, φ_{λ*}) ∈ Λ_{c,f}`, the complementary slackness
conditions (8a) `f(y) − λ* c(x, y) = sup_z {f(z) − λ* c(x, z)}` `π*`-a.s. and
(8b) `λ* (∫ c dπ* − δ) = 0` imply that `π*` and `(λ*, φ_{λ*})` are primal and dual optimizers
with `I(π*) = J(λ*, φ_{λ*})`;
4. (b, "only if") conversely, if `π*` and `(λ*, φ_{λ*})` are primal and dual optimizers with
`I(π*) = J(λ*, φ_{λ*})` **and `J(λ*, φ_{λ*}) < ∞`** (a hypothesis the page leaves implicit:
without it the "only if" fails when `I = J = ∞`), then (8a) and (8b) hold. -/
theorem theorem_1 {S : Type*} [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]
(μ : Measure S) [IsProbabilityMeasure μ] (c : S → S → ℝ) (hc : AssumptionA1 c)
(f : S → ℝ) (hf_usc : UpperSemicontinuous f) (hf_int : Integrable f μ)
(δ : ℝ) (hδ : 0 < δ) :
primalValue c f μ δ = dualValue c f μ δ ∧
(∃ lam : ℝ, 0 ≤ lam ∧ (lam, phiLam c f lam) ∈ dualFeasible c f Set.univ ∧
dualObj μ δ lam (phiLam c f lam) = dualValue c f μ δ) ∧
(∀ π ∈ primalFeasible c μ δ, ∀ lam : ℝ, (lam, phiLam c f lam) ∈ dualFeasible c f Set.univ →
((∀ᵐ p ∂π, ((f p.2 - lam * c p.1 p.2 : ℝ) : EReal) = phiLam c f lam p.1) ∧
lam * ((∫⁻ p, ENNReal.ofReal (c p.1 p.2) ∂π).toReal - δ) = 0) →
(primalObj f π = primalValue c f μ δ ∧
dualObj μ δ lam (phiLam c f lam) = dualValue c f μ δ ∧
primalObj f π = dualObj μ δ lam (phiLam c f lam))) ∧
(∀ π ∈ primalFeasible c μ δ, ∀ lam : ℝ, (lam, phiLam c f lam) ∈ dualFeasible c f Set.univ →
dualObj μ δ lam (phiLam c f lam) ≠ ⊤ →
(primalObj f π = primalValue c f μ δ ∧
dualObj μ δ lam (phiLam c f lam) = dualValue c f μ δ ∧
primalObj f π = dualObj μ δ lam (phiLam c f lam)) →
((∀ᵐ p ∂π, ((f p.2 - lam * c p.1 p.2 : ℝ) : EReal) = phiLam c f lam p.1) ∧
lam * ((∫⁻ p, ENNReal.ofReal (c p.1 p.2) ∂π).toReal - δ) = 0)) := by sorry
end ModelRiskOT.Duality