Theorem 3 — the optimal value of (3) is attained under $p'$ -growth, $p'<p$

Proved

WassersteinLinOpt.Ball.optimalValue_attained

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 3. Assume $\nu$ has a finite $p$ -th moment. If there exist $x_0\in X$ , $c>0$ and $p'\in(0,p)$ such that

f(x)\le c\,[1+d^{p'}(x,x_0)]\qquad\text{for all }x\in X,

then the optimal value of problem (3) is attained: some $\mu^\star\in\mathcal B_r(\nu)$ satisfies $\int_X f\,d\mu^\star=\sup\{\int_X f\,d\mu:\mu\in\mathcal B_r(\nu)\}$ .

Compared with Theorem 2, the growth exponent must be strictly smaller than $p$ ; the paper points to an instance with growth exponent exactly $p$ where the value is finite but not attained.

Formalization Note. "Attained" is membership in the ball together with equality of the EReal values quasiIntegral f μ = optimalValue p r ν f.

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 3, p. 1112. Under the standing assumptions of problem (3) (`f` upper
semicontinuous, quasi-integrable under every `μ ∈ 𝓑_r(ν)`), if `ν` has a finite `p`-th moment
and `f(x) ≤ c[1 + d^{p′}(x, x₀)]` for all `x`, for some `x₀ ∈ X`, `c > 0` and `p′ ∈ (0, p)`, then
the optimal value of (3) is attained by some `μ⋆ ∈ 𝓑_r(ν)`. -/
theorem optimalValue_attained {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) < ⊤)
    (x₀ : X) (c p' : ℝ) (hc : 0 < c) (hp'0 : 0 < p') (hp'p : p' < p)
    (hgrowth : ∀ x : X, f x ≤ c * (1 + dist x x₀ ^ p')) :
    ∃ μ ∈ wassersteinBall p r ν,
      quasiIntegral f (μ : Measure X) = optimalValue p r ν f := 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. 1112, Theorem 3

Read-back

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

Let $(X, d)$ be a metric space that is proper (every closed ball is compact), carrying a σ-algebra that equals its Borel σ-algebra. The statement fixes the following data and hypotheses:

real numbers $p$ and $r$ with $p \ge 1$ and $r > 0$ ;
a probability measure $\nu$ on $X$ such that $\mathrm{HasFinitePthMoment}(p, \nu)$ holds;
a function $f : X \to \mathbb{R}$ that is upper semicontinuous;
a point $x_0 \in X$ and real numbers $c$ and $p'$ with $c > 0$ and $0 < p' < p$ ;
a growth bound: for every $x \in X$ ,

f(x) \le c\,\bigl(1 + d(x, x_0)^{p'}\bigr);

a quasi-integrability hypothesis: for every $\mu$ in the set $\mathcal{B}_r(\nu) := \mathrm{wassersteinBall}(p, r, \nu)$ , with $\mu$ regarded as a measure on $X$ , at least one of the following holds:

\int_X \max\{f(x), 0\}\, d\mu(x) < \infty \quad\text{or}\quad \int_X \max\{-f(x), 0\}\, d\mu(x) < \infty.

These integrals take values in $[0, \infty]$ .

Conclusion. There is some $\mu \in \mathcal{B}_r(\nu)$ such that

\mathrm{quasiIntegral}(f, \mu) = \mathrm{optimalValue}(p, r, \nu, f).

Undefined names. Four names come from definitions that are imported but not shown here: $\mathrm{wassersteinBall}$ , $\mathrm{HasFinitePthMoment}$ , $\mathrm{optimalValue}$ and $\mathrm{quasiIntegral}$ . The last one is used without its own import line. From the code alone, all that can be said is this:

$\mathrm{wassersteinBall}(p, r, \nu)$ is a set whose elements can be viewed as measures on $X$ .
$\mathrm{HasFinitePthMoment}(p, \nu)$ is some property of the pair $(p, \nu)$ .
$\mathrm{quasiIntegral}(f, \mu)$ and $\mathrm{optimalValue}(p, r, \nu, f)$ have the same type, since the conclusion equates them.

The code does not show whether the ball uses a Wasserstein distance, whether its radius bound is $\le r$ or $< r$ , whether $\mathrm{optimalValue}$ is a supremum of $\mathrm{quasiIntegral}(f, \cdot)$ over $\mathcal{B}_r(\nu)$ , or what value $\mathrm{quasiIntegral}$ returns when both integrals above are infinite. The code does not say that $\mathrm{optimalValue}$ is finite. It also does not require $f$ to be measurable, integrable, or bounded below.

Degenerate cases.

Size of $X$ . $X$ cannot be empty, because $\nu$ is a probability measure on it. If $X$ has exactly one point, $d(x, x_0) = 0$ for every $x$ , so the growth bound becomes $f(x_0) \le c$ . The conclusion then depends only on the four imported definitions evaluated on this one-point space.
Powers of zero. At $x = x_0$ the growth bound reads $f(x_0) \le c$ , since $0^{p'} = 0$ when $p' > 0$ . Because $d \ge 0$ and $p' > 0$ , the real power $d^{p'}$ never falls back on a default value.
Empty ball. The conclusion is an existence claim inside $\mathcal{B}_r(\nu)$ . If that set were empty, the quasi-integrability hypothesis would hold vacuously and the statement would be false. Whether the set can be empty depends on the unseen definition of $\mathrm{wassersteinBall}$ .
Ranges of the parameters. $r = 0$ and $p < 1$ are excluded. $p' < p$ is strict, so $p' = p$ is excluded.
Unused hypothesis. Nothing requires $\nu$ itself to lie in $\mathcal{B}_r(\nu)$ .
Infinite values. If $\mathrm{optimalValue}$ can be $\pm\infty$ or a default value, the statement asserts that some $\mu$ in the ball gives $\mathrm{quasiIntegral}(f, \mu)$ equal to that same value. What either side returns in the infinite or undefined cases is fixed only by the unseen definitions.

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 3 — the optimal value of (3) is attained under p′p'p′-growth, p′<pp'<pp′<p

Theorem 3 — the optimal value of (3) is attained under $p'$ -growth, $p'<p$