Theorem 2 — the optimal value of (3) is finite iff $f$ has $p$ -growth

Proved

WassersteinLinOpt.Ball.optimalValue_finite_iff_growth

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

distributionally-robust-optimizationmeasure-theoryoptimal-transportwasserstein

Throughout, $(X,d)$ is a proper metric space (every closed ball is compact; such a space is complete and separable, hence Polish) with its Borel $\sigma$ -algebra, and $p \ge 1$ , $r > 0$ are real. Standing assumptions of problem (3) (p. 1108): $f$ is upper semicontinuous and, for every $\mu \in \mathcal B_r(\nu)$ , at least one of $\int_X [f]_+\,d\mu$ and $\int_X [-f]_+\,d\mu$ is finite.

Theorem 2. Assume $\nu$ has a finite $p$ -th moment. Then the optimal value

\sup\Big\{\int_X f\,d\mu:\mu\in\mathcal B_r(\nu)\Big\}

of problem (3) is finite (neither $+\infty$ nor $-\infty$ ) if and only if there exist $x_0\in X$ and $c>0$ such that $f(x)\le c\,[1+d^p(x,x_0)]$ for all $x\in X$ .

Formalization Note. The integral is the extended-real integral $\int[f]_+d\mu-\int[-f]_+d\mu$ (quasiIntegral) and the supremum is in EReal; "finite" is ≠ ⊤ ∧ ≠ ⊥. The standing quasi-integrability assumption is the hypothesis hquasi.

Preamble

import Mathlib
import Definitions.Def_WassersteinLinOpt_Ball_wassersteinBall
import Definitions.Def_WassersteinLinOpt_Ball_HasFinitePthMoment
import Definitions.Def_WassersteinLinOpt_Ball_optimalValue

open MeasureTheory
open scoped ENNReal NNReal

Formal statement

namespace WassersteinLinOpt.Ball

/-- Theorem 2, p. 1110. Let `f` be upper semicontinuous and, for every `μ ∈ 𝓑_r(ν)`, let at
least one of `∫ [f]₊ dμ`, `∫ [−f]₊ dμ` be finite (the standing assumptions of problem (3)).
If `ν` has a finite `p`-th moment, the optimal value of (3) is finite (neither `+∞` nor `−∞`)
iff `f(x) ≤ c[1 + d^p(x, x₀)]` for all `x`, for some `x₀ ∈ X` and `c > 0`. -/
theorem optimalValue_finite_iff_growth {X : Type*} [MetricSpace X] [ProperSpace X]
    [MeasurableSpace X] [BorelSpace X] (p r : ℝ) (hp : 1 ≤ p) (hr : 0 < r)
    (ν : ProbabilityMeasure X) (hν : HasFinitePthMoment p (ν : Measure X))
    (f : X → ℝ) (hf : UpperSemicontinuous f)
    (hquasi : ∀ μ ∈ wassersteinBall p r ν,
      ∫⁻ x, ENNReal.ofReal (f x) ∂(μ : Measure X) < ⊤ ∨
        ∫⁻ x, ENNReal.ofReal (-f x) ∂(μ : Measure X) < ⊤) :
    (optimalValue p r ν f ≠ ⊤ ∧ optimalValue p r ν f ≠ ⊥) ↔
      ∃ x₀ : X, ∃ c : ℝ, 0 < c ∧ ∀ x : X, f x ≤ c * (1 + dist x x₀ ^ p) := by sorry

end WassersteinLinOpt.Ball

Source

Yue, Kuhn & Wiesemann, On linear optimization over Wasserstein balls, Math. Program. 195 (2022) 1107–1122, https://doi.org/10.1007/s10107-021-01673-8, p. 1110, Theorem 2

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $X$ is a proper metric space with metric $d$ and its Borel σ-algebra. The remaining data and hypotheses are:

real numbers $p$ and $r$ with $p \ge 1$ and $r > 0$ ;
a probability measure $\nu$ with a finite $p$ -th moment, meaning some $x'$ has $\int d(x,x')^p\,d\nu < \infty$ ;
a function $f : X \to \mathbb{R}$ that is upper semicontinuous;
a quasi-integrability hypothesis: for every $\mu \in \mathcal{B}_r(\nu)$ , at least one of $\int [f]_+\,d\mu$ and $\int [-f]_+\,d\mu$ is finite.

The ball $\mathcal{B}_r(\nu)$ is the set of probability measures $\mu$ with $W_p(\mu,\nu) \le r$ , where $W_p$ is the $1/p$ -th power of the coupling infimum of $\int d^p\,d\gamma$ . The integrals of $[f]_+$ and $[-f]_+$ are $[0,+\infty]$ -valued.

The statement. Define the extended real

V = \sup_{\mu \in \mathcal{B}_r(\nu)} \Big( \int [f]_+\,d\mu - \int [-f]_+\,d\mu \Big) \in [-\infty,+\infty].

Then $V$ is neither $+\infty$ nor $-\infty$ if and only if there exist a point $x_0 \in X$ and a real $c > 0$ with

f(x) \;\le\; c\,\big(1 + d(x,x_0)^p\big) \quad \text{for all } x \in X.

Degenerate cases.

Excluded values: the hypotheses exclude $p < 1$ and $r \le 0$ .
Non-empty $X$ : the finite-moment hypothesis forces $X$ to be non-empty.
Empty ball: if $\mathcal{B}_r(\nu)$ were empty, then $V = -\infty$ and the left-hand side would be false. The statement does not itself assert that the ball is non-empty.
The value $-\infty$ : the left-hand side excludes $V = -\infty$ as well as $V = +\infty$ .
Both parts infinite: the quasi-integrability hypothesis rules out, within the ball, the case where both parts are $+\infty$ (whose difference would evaluate to $-\infty$ ).

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 2 — the optimal value of (3) is finite iff fff has ppp-growth

Theorem 2 — the optimal value of (3) is finite iff $f$ has $p$ -growth