The transport plans of two probability measures form a compact set #
The couplings of two fixed probability measures form a subset of the probability measures on the product, and the weak topology restricts to it. This file proves that this set is weakly closed and, on a Polish factor pair, weakly compact. Compactness is what makes the primal transport problem solvable: a lower semicontinuous cost attains its infimum on a nonempty compact set.
The two halves are proved at their own generality and for their own reasons.
Closedness is a statement about the marginal maps. Pushing forward along the two coordinate
projections is continuous for the weak topology, and being a coupling of μ and ν says exactly
that the two pushforwards are μ and ν; so the coupling set is an intersection of two preimages
of points. The factors and their product need measurable opens; neither Borel sigma algebras nor
second countability is needed for this argument. The set is closed as soon as points are closed in
the two spaces of marginals, which is the T1Space hypothesis carried here. Mathlib derives it from
MeasureTheory.ProbabilityMeasure.t2Space, whose hypotheses are BorelSpace together with
HasOuterApproxClosed — so it is available on the metrizable factors the later sections work
with, but is asked for explicitly here rather than assumed.
Compactness is Prokhorov's theorem. Tightness of the coupling set follows from tightness of the
two marginals alone: a compact rectangle K₁ ×ˢ K₂ misses at most the mass its two sides miss,
uniformly over all couplings, because every coupling has the same two marginals. Tightness is
therefore stated for arbitrary measures with tight marginals, and the topological hypotheses enter
only when Prokhorov's theorem is applied.
Both halves are then run with moving marginals: a family of plans that is eventually feasible for two tight families of marginals is relatively compact, and each of its weak limits along a finer filter is a coupling of the limiting marginals. Nothing about a cost function enters, which is why this lives here rather than in the stability file that consumes it.
Main statements #
TauCeti.isClosed_setOfPred_isCoupling— the couplings ofμandνare a weakly closed set of probability measures on the product, including BorelHasOuterApproxClosedfactors through typeclass inference, with a compact-pseudometrizable specialisation;TauCeti.isTightMeasureSet_setOfPred_exists_isCouplingandTauCeti.isTightMeasureSet_setOfPred_isCoupling— the couplings of two tight families of measures, and of two tight measures, form a tight family, with no topological hypothesis beyond the two topologies themselves;TauCeti.isCompact_setOfPred_isCoupling_of_prokhorov— the abstract compactness theorem for a product on which tight families of probability measures have compact closure;TauCeti.isCompact_setOfPred_isCoupling— the Prokhorov theorem for a Hausdorff Borel product, with compact-metrizable and Polish specialisations;TauCeti.isCoupling_of_tendsto— the coupling constraint passes to weak limits when the marginals converge;TauCeti.exists_isCoupling_tendsto_of_isTightMeasureSet— relative compactness of a family of plans with tight varying marginals;TauCeti.Coupling.instCompactSpace— the bundled couplings of inner-regular probability measures form a compact space when the factors are Hausdorff with measurable opens, the product is Borel, and both spaces of marginal probability measures areT1.
References #
- C. Villani, Optimal Transport: Old and New, Springer 2009, Chapter 4 — the tightness lemma for transference plans that precedes the existence theorem for an optimal coupling.
- F. Santambrogio, Optimal Transport for Applied Mathematicians, Springer 2015, Chapter 1 — the same compactness argument, run through Prokhorov's theorem.
The couplings of two probability measures are weakly closed. The coupling set is the
intersection of the preimages of {μ} and {ν} under the two marginal maps, both of which are
continuous for the topology of convergence in distribution. The T1Space hypotheses are what make
the two singletons closed. They hold for Borel factors with HasOuterApproxClosed, in particular
for pseudometrizable Borel factors, by MeasureTheory.ProbabilityMeasure.t2Space. The factors and
their product need only measurable opens for the marginal maps to be continuous.
The couplings of two tight families of measures form a tight family. A coupling gives the complement of a compact rectangle at most the mass its two marginals give the complements of the two sides, and those bounds are uniform over the two families because a coupling is exhausted by its marginals. No hypothesis beyond the two topologies is needed. The marginals are allowed to range over sets rather than to be fixed, which is what a stability argument with moving marginals consumes.
The couplings of two tight measures form a tight family. This is the fixed-marginal case of
TauCeti.isTightMeasureSet_setOfPred_exists_isCoupling, and it is the tightness that Prokhorov's
theorem is applied to below.
The abstract theorem exposes exactly the Prokhorov property used by the coupling argument: every tight family of probability measures on the product has compact closure.
Compactness of couplings under an abstract Prokhorov property. If every tight family of probability measures on the product has compact closure, then the couplings of two tight marginals form a compact set. This keeps the compactness argument available beyond the concrete Hausdorff Borel version of Prokhorov's theorem without inferring the property from Radon regularity.
Prokhorov's theorem asks the product to be Hausdorff and Borel. Assuming BorelSpace for the
product directly avoids imposing second countability on either factor. Closedness additionally
asks that the two spaces of probability measures be T1; these hypotheses do not choose a metric
on either factor.
The couplings of two tight probability measures are weakly compact. The set is tight by
TauCeti.isTightMeasureSet_setOfPred_isCoupling, hence relatively compact by Prokhorov's theorem,
and it is closed by TauCeti.isClosed_setOfPred_isCoupling; so it equals its own closure and is
compact. Hausdorffness is required only of the product.
The bundled couplings of two inner-regular probability measures form a compact space for weak
convergence when both factors are Hausdorff with measurable opens, their product is a Borel space,
and both spaces of marginal probability measures are T1. This applies in particular to
probability measures on Polish Borel spaces.
Weak limits of plans whose marginals move. The hypotheses are those of the two sections above,
strengthened from T1 to T2 on the two spaces of marginals because a limit is identified here,
not merely trapped in a closed set. Passing to limits needs only measurable opens on the factors
and product; extracting a convergent refinement additionally needs a Hausdorff Borel product.
The coupling constraint passes to weak limits. If the plans πs i are eventually couplings
of μs i and νs i, and the plans and both marginals converge weakly along the same filter,
then the limiting plan is a coupling of the limiting marginals.
The two marginal maps are weakly continuous, so this is uniqueness of weak limits applied to the
two marginals of πs.
Relative compactness of a family of transport plans with moving marginals. If a tail of each marginal family is tight, then any eventually feasible family of plans has a weakly convergent refinement whose limit is a coupling of the limiting marginals. Prokhorov's theorem needs Hausdorffness and the Borel sigma algebra only on the product; no second-countability hypothesis on either factor is required.
Closedness of couplings on compact pseudometrizable spaces. This is the directly usable
compact-pseudometrizable specialisation of TauCeti.isClosed_setOfPred_isCoupling.
Compactness of couplings on compact metrizable spaces. Compactness makes every family of measures tight, so the general coupling compactness theorem applies without marginal hypotheses.
The Polish specialisation is stated for Mathlib's PolishSpace, the topological notion: second
countable and completely metrizable, with no distance chosen. That is what makes the two factors
tight and hence the coupling set compact.
The couplings of two probability measures on Polish spaces are weakly compact. On a Polish
space every finite Borel measure is tight, so the tightness hypotheses of
TauCeti.isCompact_setOfPred_isCoupling are automatic. This is the compactness that the direct
method of the calculus of variations consumes.