Lemma 3 — Portmanteau characterization by upper semicontinuous functions

Proved

WassersteinLinOpt.Ball.tendsto_iff_limsup_quasiIntegral_le

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 3. A sequence $(\mu^k)_k$ in $\mathcal P(X)$ converges weakly to $\mu^\infty\in\mathcal P(X)$ if and only if for every function $g:X\to\mathbb R$ that is bounded above and upper semicontinuous,

\limsup_{k\to\infty}\int_X g\,d\mu^k\le\int_X g\,d\mu^\infty .

This excerpt of the Portmanteau theorem is what Theorem 3's proof uses for a truncated objective.

Formalization Note. Weak convergence is Filter.Tendsto μs atTop (nhds μlim) in ProbabilityMeasure X. Since $g$ is bounded above, $\int[g]_+$ is finite and the integral is a well-defined value in $[-\infty,\infty)$ , taken as quasiIntegral in EReal; the $\limsup$ is Filter.limsup in EReal.

Preamble

import Mathlib
import Definitions.Def_WassersteinLinOpt_Ball_quasiIntegral

open MeasureTheory
open scoped ENNReal NNReal

Formal statement

namespace WassersteinLinOpt.Ball

/-- Lemma 3 (Appendix A, p. 1120; excerpted from the Portmanteau theorem). A sequence `μᵏ` in
`𝒫(X)` converges weakly to `μ^∞` iff `limsup_k ∫ g dμᵏ ≤ ∫ g dμ^∞` for every upper-bounded,
upper semicontinuous `g : X → ℝ`. The integrals are extended-real (they may be `−∞`). -/
theorem tendsto_iff_limsup_quasiIntegral_le {X : Type*} [MetricSpace X] [ProperSpace X]
    [MeasurableSpace X] [BorelSpace X] (μs : ℕ → ProbabilityMeasure X)
    (μlim : ProbabilityMeasure X) :
    Filter.Tendsto μs Filter.atTop (nhds μlim) ↔
      ∀ g : X → ℝ, BddAbove (Set.range g) → UpperSemicontinuous g →
        Filter.limsup (fun k => quasiIntegral g (μs k : Measure X)) Filter.atTop ≤
          quasiIntegral g (μlim : Measure X) := 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. 1120, Lemma 3 (Appendix A)

Read-back

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

Setting. $X$ is a proper metric space with its Borel σ-algebra. The inputs are a sequence $\mu_1, \mu_2, \dots$ of probability measures on $X$ and a probability measure $\mu^\infty$ on $X$ .

The statement. The following two conditions are equivalent.

$\mu_k \to \mu^\infty$ as $k \to \infty$ in Mathlib's topology on probability measures. This is the weak-convergence topology, generated by $\mu \mapsto \int h\,d\mu$ for bounded continuous $h : X\to[0,\infty)$ .
For every function $g : X \to \mathbb{R}$ that is bounded above and upper semicontinuous,

\limsup_{k\to\infty} \Big(\int [g]_+\,d\mu_k - \int [-g]_+\,d\mu_k\Big) \;\le\; \int [g]_+\,d\mu^\infty - \int [-g]_+\,d\mu^\infty.

The integrals are $[0,+\infty]$ -valued. The differences and the limit superior are computed in the extended reals $[-\infty,+\infty]$ .

Degenerate cases.

Finite positive part: because $g$ is bounded above and the measures are probability measures, each positive part $\int [g]_+$ is finite. Each difference therefore lies in $[-\infty, +\infty)$ , and the evaluation of $(+\infty) - (+\infty)$ to $-\infty$ never occurs.
Differences equal to $-\infty$ : a difference is $-\infty$ exactly when $\int [-g]_+ = +\infty$ .
$X$ empty: there are no probability measures, so the statement is vacuous.

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