Prove2Me

Proposition 7 — inf⁡(λ,φ)∈Λ(Sπ×Sπ)J(λ,φ)≤I\inf_{(\lambda,\varphi)\in\Lambda(S_\pi\times S_\pi)}J(\lambda,\varphi)\le I

Open
ModelRiskOT.Duality.proposition_7

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

dualityoptimal-transportp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let SS be a Polish space, μ\mu a Borel probability measure on SS, c:S×S→[0,∞)c : S\times S\to[0,\infty) a lower semicontinuous cost with c(x,y)=0c(x,y)=0 if and only if x=yx=y (Assumption (A1)), f:S→Rf : S\to\mathbb R upper semicontinuous and μ\mu-integrable (Assumption (A2)), and δ>0\delta>0. Let π\pi be a probability measure on S×SS\times S such that

  1. (a) ∫c(x,y) dπ(x,y)<∞\int c(x,y)\,d\pi(x,y)<\infty;
  2. (b) ∫f(y) dπ(x,y)∈(−∞,∞)\int f(y)\,d\pi(x,y)\in(-\infty,\infty);
  3. (c) π(A×S)=μ(A)\pi(A\times S)=\mu(A) for every Borel set A⊆SA\subseteq S.

Let Sπ=Spt(πX)∪Spt(πY)S_\pi=\mathrm{Spt}(\pi_X)\cup\mathrm{Spt}(\pi_Y) and let Λ(Sπ×Sπ)\Lambda(S_\pi\times S_\pi) be the set of pairs (λ,φ)(\lambda,\varphi) with λ≥0\lambda\ge0, φ\varphi universally measurable and φ(x)+λc(x,y)≥f(y)\varphi(x)+\lambda c(x,y)\ge f(y) for all x,y∈Sπx,y\in S_\pi (29). Then

inf⁡(λ,φ)∈Λ(Sπ×Sπ)(λδ+∫φ dμ)≤I.\inf_{(\lambda,\varphi)\in\Lambda(S_\pi\times S_\pi)}\Big(\lambda\delta+\int\varphi\,d\mu\Big)\le I.

Note that π\pi is not required to satisfy the budget ∫c dπ≤δ\int c\,d\pi\le\delta. Proposition 7 carries the compact duality of Proposition 6 to the σ\sigma-compact set Sπ×SπS_\pi\times S_\pi.

Formalization Note The space SS is a Polish space with its Borel σ-algebra; the cost cc is real-valued and written curried, c x y=c(x,y)c\,x\,y = c(x,y); (A1) is the structure AssumptionA1; (A2) is the pair of hypotheses UpperSemicontinuous f and Integrable f μ. Values that can be infinite (II, JJ, I(π)I(\pi), J(λ,φ)J(\lambda,\varphi), φλ\varphi_\lambda) live in EReal; an integral of an extended-real function is ∫φ+−∫φ−\int\varphi^+ - \int\varphi^- with lower Lebesgue integrals, and ∞−∞\infty-\infty evaluates to −∞-\infty, so a coupling with ∫f− dπ=∞\int f^-\,d\pi=\infty never raises the primal supremum (the paper's footnote 2 reading).

Preamble
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_admissibleSet

open MeasureTheory
Formal statement
namespace ModelRiskOT.Duality

/-- **Proposition 7** (Blanchet & Murthy, arXiv:1604.01446v2, §4.3, p. 20). Under (A1) and (A2),
with `δ > 0`: let `π` be a probability measure on `S × S` with (a) `∫ c dπ < ∞`,
(b) `∫ f(y) dπ(x, y) ∈ (−∞, ∞)` and (c) `π(A × S) = μ(A)` for every Borel `A`. Then
`inf_{(λ, φ) ∈ Λ(S_π × S_π)} J(λ, φ) ≤ I`, where `S_π = Spt(π_X) ∪ Spt(π_Y)` and `Λ(K × K)` is
(29). No budget constraint `∫ c dπ ≤ δ` is assumed. -/
theorem proposition_7 {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 < δ)
    (π : Measure (S × S)) [IsProbabilityMeasure π]
    (ha : ∫⁻ p, ENNReal.ofReal (c p.1 p.2) ∂π < ⊤)
    (hb : Integrable (fun p => f p.2) π)
    (hmarg : ∀ A : Set S, MeasurableSet A → π (A ×ˢ Set.univ) = μ A) :
    (⨅ p ∈ dualFeasible c f (supportUnion π), dualObj μ δ p.1 p.2) ≤ primalValue c f μ δ := by sorry

end ModelRiskOT.Duality
Source
Blanchet & Murthy, Quantifying Distributional Model Risk via Optimal Transport, arXiv:1604.01446v2, p. 20, §4.3, Proposition 7 (with (29) and §4.2's S_π)

View graph