Lemma 1 — the Wasserstein ball has a uniformly bounded $p$ -th moment

Proved

WassersteinLinOpt.Ball.ball_uniformly_bounded_moment

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.

Lemma 1. Let $\nu\in\mathcal P(X)$ have a finite $p$ -th moment. Then for every $x_0\in X$ there is a constant $C>0$ such that

\int_X d^p(x,x_0)\,d\mu(x)\le C\qquad\text{for all }\mu\in\mathcal B_r(\nu).

In particular every measure in the ball has a finite $p$ -th moment. The lemma feeds the tightness argument of Theorem 1 and the truncation estimate of Theorem 3.

Formalization Note. The paper leaves $x_0$ free; the statement is given for every $x_0$ (the choice does not matter, p. 1109), which is the form Theorem 3's proof uses. $C$ is only asserted to exist; it may depend on $p$ , $r$ , $\nu$ and $x_0$ . The moment is a lower Lebesgue integral in ℝ≥0∞.

Preamble

import Mathlib
import Definitions.Def_WassersteinLinOpt_Ball_wassersteinBall
import Definitions.Def_WassersteinLinOpt_Ball_HasFinitePthMoment

open MeasureTheory
open scoped ENNReal NNReal

Formal statement

namespace WassersteinLinOpt.Ball

/-- Lemma 1 (Yue–Kuhn–Wiesemann 2022, p. 1109). If `ν` has a finite `p`-th moment, then the
Wasserstein ball `𝓑_r(ν)` has a uniformly bounded `p`-th moment: for every reference point
`x₀` there is `C > 0` with `∫_X d^p(x, x₀) dμ(x) ≤ C` for all `μ ∈ 𝓑_r(ν)`. -/
theorem ball_uniformly_bounded_moment {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)) (x₀ : X) :
    ∃ C : ℝ, 0 < C ∧ ∀ μ ∈ wassersteinBall p r ν,
      ∫⁻ x, ENNReal.ofReal (dist x x₀ ^ p) ∂(μ : Measure X) ≤ ENNReal.ofReal C := 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. 1109, Lemma 1

Read-back

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

Setting. $X$ is a metric space with metric $d$ , equipped with its Borel σ-algebra. It is proper: every closed ball is compact. The remaining data and hypotheses are:

real numbers $p$ and $r$ with $p \ge 1$ and $r > 0$ ;
a probability measure $\nu$ on $X$ with a finite $p$ -th moment, meaning some $x' \in X$ has $\int d(x,x')^p\,d\nu(x) < \infty$ ;
an arbitrary point $x_0 \in X$ .

The statement. There exists a real number $C > 0$ such that every probability measure $\mu$ with $W_p(\mu,\nu) \le r$ satisfies

\int_X d(x,x_0)^p\, d\mu(x) \;\le\; C.

Here:

the integral is $[0,+\infty]$ -valued, so the inequality in particular says that it is finite;
$W_p(\mu,\nu)$ is the $1/p$ -th power of the infimum, over measures $\gamma$ on $X\times X$ with first marginal $\mu$ and second marginal $\nu$ , of $\int d(x_1,x_2)^p\,d\gamma$ , computed in $[0,+\infty]$ ;
the constant $C$ may depend on $p$ , $r$ , $\nu$ and $x_0$ ;
$C$ must be the same for all $\mu$ in the ball.

Degenerate cases. The hypotheses exclude $p < 1$ and $r \le 0$ . $X$ cannot be empty, because the point $x_0$ is given. No other degenerate case is permitted.

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

Lemma 1 — the Wasserstein ball has a uniformly bounded ppp-th moment

Lemma 1 — the Wasserstein ball has a uniformly bounded $p$ -th moment