Theorem 1 — weak compactness of the Wasserstein ball

Proved

WassersteinLinOpt.Ball.ball_isCompact

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.

Theorem 1 (Weak Compactness of Wasserstein Ball). If $\nu\in\mathcal P(X)$ has a finite $p$ -th moment, then the Wasserstein ball

\mathcal B_r(\nu)=\{\mu\in\mathcal P(X):W_p(\mu,\nu)\le r\}

is compact in the weak topology of $\mathcal P(X)$ .

Compactness is what makes the existence results of Sections 4 and 5 possible.

Formalization Note. $\mathcal P(X)$ is Mathlib's ProbabilityMeasure X with its topology of convergence against bounded continuous functions, i.e. the paper's weak convergence (Definition 2). The paper's weak compactness is sequential (Definition 3); since $\mathcal P(X)$ is metrizable (p. 1120) the two notions agree, and the statement uses IsCompact.

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

/-- Theorem 1 (Weak Compactness of Wasserstein Ball), p. 1109. On a proper metric space, the
Wasserstein ball `𝓑_r(ν)` is compact in the weak topology of `𝒫(X)` whenever `ν` has a
finite `p`-th moment. -/
theorem ball_isCompact {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)) :
    IsCompact (wassersteinBall p r ν) := 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, Theorem 1

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$ , equipped with 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$ on $X$ with a finite $p$ -th moment, meaning some $x_0$ has $\int d(x,x_0)^p\,d\nu < \infty$ .

The statement. The set

\mathcal{B}_r(\nu) = \{\mu \text{ a probability measure on } X : W_p(\mu,\nu) \le r\}

is a compact subset of the space of probability measures on $X$ .

The space of probability measures carries Mathlib's standard topology. This is the topology of weak convergence: the coarsest topology making $\mu \mapsto \int h\,d\mu$ continuous for every bounded continuous function $h : X \to [0,\infty)$ .
$W_p(\mu,\nu)$ is the $1/p$ -th power of the infimum over couplings $\gamma$ of $(\mu,\nu)$ of $\int d(x_1,x_2)^p\,d\gamma$ , computed in $[0,+\infty]$ .

Degenerate cases. The hypotheses exclude $p < 1$ and $r \le 0$ . The finite-moment hypothesis forces $X$ to be non-empty. Compactness includes the case where the ball is empty, but that case does not arise, because $W_p(\nu,\nu)$ is never examined here and only the compactness claim is made.

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