Wasserstein convergence implies weak convergence

Convergence in any p-Wasserstein distance with 1 ≤ p is stronger than weak convergence of probability measures. This file proves that implication through the Lévy--Prokhorov metric.

The quantitative input is the classical coupling estimate: if a coupling has expected displacement less than ε², then its marginals are at Lévy--Prokhorov distance at most ε. Markov's inequality bounds the mass of pairs whose displacement exceeds the thickening radius. Monotonicity of eLpNorm then lets the same estimate consume a p-Wasserstein bound for every 1 ≤ p, including p = ∞.

On a separable Borel pseudometric space, the Lévy--Prokhorov metric induces the weak topology. Consequently, the inclusions of both finite-moment Wasserstein spaces and arbitrary anchored finite-distance components into ProbabilityMeasure are continuous.

Main statements

• TauCeti.wassersteinEDist_map_le_of_edist_le — an almost-everywhere displacement bound for the Wasserstein distance to a pushforward;
• TauCeti.levyProkhorovEDist_le_of_wassersteinEDist_lt_mul_self — a quantitative comparison between the two extended distances;
• TauCeti.WassersteinSpace.continuous_toProbabilityMeasure — Wasserstein convergence of finite-moment laws implies weak convergence;
• TauCeti.WassersteinComponent.continuous_toProbabilityMeasure — the same implication on an arbitrary finite-distance component.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 6.
• P. Billingsley, Convergence of Probability Measures, Wiley, 1999, Chapter 1.

theorem TauCeti.wassersteinEDist_map_le_of_edist_le {Z : Type u_1} [PseudoMetricSpace Z] [SecondCountableTopology Z] [MeasurableSpace Z] [BorelSpace Z] (ρ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure ρ] {F : Z → Z} (hF : AEMeasurable F ρ) {δ : ENNReal} (hδ : ∀ᵐ (z : Z) ∂ρ, edist z (F z) ≤ δ) : wassersteinEDist 1 ρ (MeasureTheory.Measure.map F ρ) ≤ δ

If an almost-everywhere measurable map moves almost every point by at most δ, its pushforward is at most δ away in the first Wasserstein distance.

theorem TauCeti.levyProkhorovEDist_le_of_wassersteinEDist_lt_mul_self {X : Type u} [PseudoEMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {p ε : ENNReal} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) (h : wassersteinEDist p μ ν < ε * ε) : MeasureTheory.levyProkhorovEDist μ ν ≤ ε

If the p-Wasserstein distance is strictly below ε², then the Lévy--Prokhorov extended distance is at most ε, for 1 ≤ p.

The square is not asserted to be an optimal modulus. It is the direct consequence of Markov's inequality needed to compare the Wasserstein and weak topologies.

theorem TauCeti.WassersteinSpace.continuous_toProbabilityMeasure {X : Type u} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] : Continuous toProbabilityMeasure

The inclusion of the finite-moment p-Wasserstein space into probability measures is continuous when the codomain carries its weak topology.

theorem TauCeti.WassersteinComponent.continuous_toProbabilityMeasure {X : Type u} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} : Continuous toProbabilityMeasure

The inclusion of an anchored finite-distance p-Wasserstein component into probability measures is continuous when the codomain carries its weak topology.