Wasserstein convergence and convergence of moments

For a finite exponent 1 ≤ p < ∞, convergence in the p-Wasserstein distance is weak convergence of probability measures together with convergence of the p-moments. This file proves both halves of this classical characterization and assembles them on the finite-moment Wasserstein space TauCeti.WassersteinSpace p X over a separable Borel pseudometric space.

The moment of a law about a basepoint x is its Wasserstein distance from the Dirac law at x (TauCeti.wassersteinEDist_dirac_left), so the triangle inequality makes it a continuous function on the Wasserstein space; this holds for every exponent, including p = ∞, in its eLpNorm form. Together with TauCeti.WassersteinSpace.continuous_toProbabilityMeasure, which gives weak convergence, this is the necessity half. Uniform integrability of the tails then follows from the general criterion TauCeti.exists_setLIntegral_le_of_tendsto_lintegral for integrals of unbounded continuous functions along weakly convergent families.

For the sufficiency half, a displacement larger than 2 R forces one of the two endpoints to lie at distance at least R from the basepoint, and then the displacement is at most twice that distance. The p-th power of the displacement is therefore at most its truncation at 2 R plus 2 ^ p times the p-moment tails beyond R of the two marginals (TauCeti.edist_rpow_le_min_add_indicator). The tails are uniformly small by the uniform integrability just described, and the transport cost of the bounded truncated cost tends to 0 along weak convergence by TauCeti.tendsto_transportCost_of_tendsto_probabilityMeasure.

Main statements

• TauCeti.WassersteinSpace.continuous_eLpNorm_edist — the L^p norm of the distance to a basepoint is continuous on the Wasserstein space;
• TauCeti.WassersteinSpace.continuous_lintegral_edist_rpow — for p < ∞, so is the p-moment ∫⁻ y, edist x y ^ p;
• TauCeti.WassersteinSpace.continuous_integral_dist_rpow — the same for the real-valued p-moment ∫ y, dist y x ^ p, which is integrable by TauCeti.WassersteinSpace.integrable_dist_rpow;
• TauCeti.exists_setLIntegral_edist_rpow_le_of_tendsto_lintegral — along a weakly convergent family whose p-moments converge to a finite limit, the p-moments have uniformly small tails;
• TauCeti.WassersteinSpace.exists_setLIntegral_edist_rpow_le — in particular, the p-moments have uniformly small tails along a W_p-convergent family;
• TauCeti.tendsto_wassersteinEDist_of_tendsto_probabilityMeasure_of_tendsto_lintegral — on a separable pseudometric space, weak convergence together with convergence of the p-moments to a finite limit gives convergence in the p-Wasserstein distance, for every finite nonzero exponent;
• TauCeti.WassersteinSpace.tendsto_iff_tendsto_toProbabilityMeasure_and_lintegral — the characterization of convergence in the Wasserstein space.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Definition 6.8 and Theorem 6.9.
• L. Ambrosio, N. Gigli and G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd edition, Birkhäuser 2008, Proposition 7.1.5.

theorem TauCeti.exists_setLIntegral_edist_rpow_le_of_tendsto_lintegral {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {p : ENNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure X} {μ : MeasureTheory.ProbabilityMeasure X} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (h : Filter.Tendsto μs L (nhds μ)) (x : X) (hμ : ∫⁻ (y : X), edist x y ^ p.toReal ∂↑μ ≠ ⊤) (hlim : Filter.Tendsto (fun (i : γ) => ∫⁻ (y : X), edist x y ^ p.toReal ∂↑(μs i)) L (nhds (∫⁻ (y : X), edist x y ^ p.toReal ∂↑μ))) {ε : ENNReal} (hε : 0 < ε) : ∃ (R : NNReal), ∀ᶠ (i : γ) in L, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑(μs i) ≤ ε

Uniformly small moment tails. For a finite nonzero exponent p, along a weakly convergent family of probability measures whose p-moments about a basepoint converge to the finite p-moment of the limit, the p-moments have uniformly small tails: for every ε > 0 there is a radius R such that eventually the part of the p-moment coming from distance at least R is at most ε.

theorem TauCeti.lowerSemicontinuous_setLIntegral_edist_rpow {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {q : ℝ} (x : X) (r : NNReal) : LowerSemicontinuous fun (ν : MeasureTheory.ProbabilityMeasure X) => ∫⁻ (y : X) in {y : X | r < nndist x y}, edist x y ^ q ∂↑ν

The part of a moment coming from the open region beyond a radius is a weakly lower semicontinuous function of the law, its integrand being lower semicontinuous.

theorem TauCeti.lintegral_edist_rpow_le_add {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {q : ℝ} (hq : 0 ≤ q) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] (x : X) (r : NNReal) : ∫⁻ (y : X), edist x y ^ q ∂ν ≤ ↑r ^ q + ∫⁻ (y : X) in {y : X | r < nndist x y}, edist x y ^ q ∂ν

A moment of a probability measure is at most the q-th power of a radius plus the part of the moment coming from the open region beyond that radius.

theorem TauCeti.tendsto_lintegral_edist_rpow {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {q : ℝ} (hq : 0 < q) {γ : Type u_3} {L : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure X} {μ : MeasureTheory.ProbabilityMeasure X} (h : Filter.Tendsto μs L (nhds μ)) (x : X) (htail : ∀ (ε : ENNReal), 0 < ε → ∃ (r : NNReal), ∀ᶠ (i : γ) in L, ∫⁻ (y : X) in {y : X | r < nndist x y}, edist x y ^ q ∂↑(μs i) ≤ ε) : Filter.Tendsto (fun (i : γ) => ∫⁻ (y : X), edist x y ^ q ∂↑(μs i)) L (nhds (∫⁻ (y : X), edist x y ^ q ∂↑μ))

Along a weakly convergent family of laws whose q-moments have uniformly small tails over the open regions beyond some radii, the q-moments converge to the q-moment of the limit.

theorem TauCeti.WassersteinSpace.continuous_eLpNorm_edist {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (x : X) : Continuous fun (μ : WassersteinSpace p X) => MeasureTheory.eLpNorm (fun (y : X) => edist x y) p ↑↑μ

The L^p norm of the distance to a basepoint, that is the p-th root of the p-moment about that basepoint, is continuous on the Wasserstein space: it is the Wasserstein distance from the Dirac law at the basepoint.

theorem TauCeti.WassersteinSpace.continuous_lintegral_edist_rpow {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : X) : Continuous fun (μ : WassersteinSpace p X) => ∫⁻ (y : X), edist x y ^ p.toReal ∂↑↑μ

For a finite exponent p, the p-moment ∫⁻ y, edist x y ^ p about a basepoint is a continuous function on the p-Wasserstein space.

theorem TauCeti.WassersteinSpace.integrable_dist_rpow {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (μ : WassersteinSpace p X) (x : X) : MeasureTheory.Integrable (fun (y : X) => dist y x ^ p.toReal) ↑↑μ

For a finite exponent, the p-th power of the distance to a basepoint is integrable against every law with finite p-moment.

theorem TauCeti.WassersteinSpace.continuous_integral_dist_rpow {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : X) : Continuous fun (μ : WassersteinSpace p X) => ∫ (y : X), dist y x ^ p.toReal ∂↑↑μ

For a finite exponent, the integral ∫ d(y, x)^p dμ(y) of the p-th power of the distance to a basepoint is a continuous real function on the p-Wasserstein space.

theorem TauCeti.WassersteinSpace.exists_setLIntegral_edist_rpow_le {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) {γ : Type u_2} {L : Filter γ} {μs : γ → WassersteinSpace p X} {μ : WassersteinSpace p X} (h : Filter.Tendsto μs L (nhds μ)) (x : X) {ε : ENNReal} (hε : 0 < ε) : ∃ (R : NNReal), ∀ᶠ (i : γ) in L, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑(μs i) ≤ ε

Uniform integrability of moments along a W_p-convergent family. For a finite exponent 1 ≤ p < ∞, along a family converging in the p-Wasserstein distance the p-moments about any basepoint have uniformly small tails: for every ε > 0 there is a radius R such that eventually the part of the p-moment coming from distance at least R is at most ε.

theorem TauCeti.tendsto_wassersteinEDist_of_tendsto_probabilityMeasure_of_tendsto_lintegral {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {p : ENNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure X} {μ : MeasureTheory.ProbabilityMeasure X} [TopologicalSpace.SeparableSpace X] (hp0 : p ≠ 0) (hp : p ≠ ⊤) (h : Filter.Tendsto μs L (nhds μ)) (x : X) (hμ : ∫⁻ (y : X), edist x y ^ p.toReal ∂↑μ ≠ ⊤) (hlim : Filter.Tendsto (fun (i : γ) => ∫⁻ (y : X), edist x y ^ p.toReal ∂↑(μs i)) L (nhds (∫⁻ (y : X), edist x y ^ p.toReal ∂↑μ))) : Filter.Tendsto (fun (i : γ) => wassersteinEDist p ↑(μs i) ↑μ) L (nhds 0)

Weak convergence and convergence of moments give Wasserstein convergence. On a separable pseudometric space, let probability measures μᵢ converge weakly to μ, and let their p-moments about a basepoint x converge to the finite p-moment of μ. Then for every finite nonzero exponent p the p-Wasserstein distance from μᵢ to μ tends to 0.

theorem TauCeti.WassersteinSpace.tendsto_iff_tendsto_toProbabilityMeasure_and_lintegral {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) {γ : Type u_2} {L : Filter γ} {μs : γ → WassersteinSpace p X} {μ : WassersteinSpace p X} (x : X) : Filter.Tendsto μs L (nhds μ) ↔ Filter.Tendsto (fun (i : γ) => ↑(μs i)) L (nhds ↑μ) ∧ Filter.Tendsto (fun (i : γ) => ∫⁻ (y : X), edist x y ^ p.toReal ∂↑↑(μs i)) L (nhds (∫⁻ (y : X), edist x y ^ p.toReal ∂↑↑μ))

Convergence in the Wasserstein space. For a finite exponent 1 ≤ p < ∞ and any basepoint x, a family of finite-moment laws converges in the p-Wasserstein distance exactly when it converges weakly and its p-moments about x converge to the p-moment of the limit.