Lemma 4.16 — tightness of transference plans

Proved

MongeKantorovichYao.transferencePlansOf_isTight

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

measure-theoryoptimal-transporttightness

Let $X,Y$ be Polish spaces with their Borel σ-algebras, and let $M\subseteq\mathcal P(X)$ and $N\subseteq\mathcal P(Y)$ be tight sets of probability measures: for every $\varepsilon>0$ there is a compact $K\subseteq X$ with $\mu(X\setminus K)<\varepsilon$ for all $\mu\in M$ , and similarly for $N$ . Let $\Pi(M,N)$ be the set of probability measures on $X\times Y$ whose marginals on $X$ and $Y$ lie in $M$ and $N$ respectively. Then $\Pi(M,N)$ is tight in $\mathcal P(X\times Y)$ .

Combined with Prokhorov's theorem, this yields convergent subsequences of transference plans, which is how the discrete case is passed to the limit.

Formalization Note Tightness is Mathlib's IsTightMeasureSet, which is equivalent to the $\varepsilon$ –compact-set formulation of Definition 4.9.

Preamble

import Mathlib
import Definitions.Def_MongeKantorovichYao_Defs

open MeasureTheory

Formal statement

namespace MongeKantorovichYao

theorem transferencePlansOf_isTight {X Y : Type*}
    [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y]
    (M : Set (Measure X)) (N : Set (Measure Y))
    (hMprob : ∀ μ ∈ M, IsProbabilityMeasure μ) (hNprob : ∀ ν ∈ N, IsProbabilityMeasure ν)
    (hM : IsTightMeasureSet M) (hN : IsTightMeasureSet N) :
    IsTightMeasureSet (transferencePlansOf M N) := by sorry

end MongeKantorovichYao

Source

Colin Yao, *Monge–Kantorovich and Transportation Theory* (paper dated September 10, 2023), p. 10, Lemma 4.16 (tightness of transference), with Definition 4.9

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (same agent as the drafter; non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves (or obtain an independent read-back).

Data and hypotheses. Polish spaces $X,Y$ with Borel σ-algebras; a set $M$ of measures on $X$ and a set $N$ of measures on $Y$ ; every element of $M$ and of $N$ is a probability measure; $M$ is tight and $N$ is tight, where a set $S$ of measures is tight if $\sup_{m\in S}m(K^c)\to 0$ as $K$ runs through compact sets (i.e. for every $\varepsilon>0$ there is a compact $K$ with $m(K^c)\le\varepsilon$ for all $m\in S$ ).

Conclusion. The set of all probability measures $\pi$ on $X\times Y$ whose first-coordinate pushforward belongs to $M$ and whose second-coordinate pushforward belongs to $N$ is tight in the same sense (compact sets of $X\times Y$ ).

Edge cases. $M$ or $N$ may be empty, in which case the set of plans is empty and trivially tight.

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph