Bounded transport costs along weakly convergent marginals

A cost c : X × X → ℝ≥0∞ that is bounded and vanishes uniformly near the diagonal — for every ε > 0 there is δ > 0 with c (x, y) ≤ ε whenever edist x y < δ — measures how far apart two laws are. This file proves that on a separable pseudometric space every such transport cost tends to 0 along a weakly convergent family of probability measures: if μᵢ ⇀ μ, then transportCost c μᵢ μ → 0. Bounded costs such as min (edist x y) R ^ p are the truncations through which the convergence of Wasserstein distances is reduced to weak convergence and the convergence of moments.

The proof transports mass cell by cell along a finite partition of the space, using the deterministic estimate TauCeti.transportCost_le_sum_of_partition. The cells are the pieces cut out by finitely many small balls centred at the points of a dense sequence, with radii chosen so that the limit law does not charge any of the bounding spheres. The masses of such cells converge by the portmanteau theorem, so the excess mass tends to 0, while the balls leave only a small mass of the limit law outside them.

Main statements

• TauCeti.tendsto_transportCost_of_tendsto_probabilityMeasure — a bounded cost vanishing uniformly near the diagonal has transport cost tending to 0 along a weakly convergent family.
• TauCeti.tendsto_transportCost_min_edist_rpow_of_tendsto_probabilityMeasure — in particular, so does the truncated power cost min (edist x y) C ^ p for a finite nonzero exponent p.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Theorem 6.9, where weak convergence together with convergence of moments is shown to give Wasserstein convergence.
• 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.
• P. Billingsley, Convergence of Probability Measures, 2nd edition, Wiley 1999, Theorem 2.1, the portmanteau theorem for sets whose boundary is not charged by the limit law.

theorem TauCeti.tendsto_transportCost_of_tendsto_probabilityMeasure {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] {c : X × X → ENNReal} {M : ENNReal} (hM_top : M ≠ ⊤) (hM : ∀ (z : X × X), c z ≤ M) (hc : ∀ ε > 0, ∃ δ > 0, ∀ (x y : X), edist x y < δ → c (x, y) ≤ ε) {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure X} {μ : MeasureTheory.ProbabilityMeasure X} (h : Filter.Tendsto μs L (nhds μ)) : Filter.Tendsto (fun (i : γ) => transportCost c ↑(μs i) ↑μ) L (nhds 0)

Bounded transport costs along weak convergence. On a separable pseudometric space, let c : X × X → ℝ≥0∞ be a bounded cost vanishing uniformly near the diagonal: for every ε > 0 there is δ > 0 such that c (x, y) ≤ ε whenever edist x y < δ. If probability measures μᵢ converge weakly to μ, then the transport cost of c from μᵢ to μ tends to 0.

theorem TauCeti.tendsto_transportCost_min_edist_rpow_of_tendsto_probabilityMeasure {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (C : NNReal) {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure X} {μ : MeasureTheory.ProbabilityMeasure X} (h : Filter.Tendsto μs L (nhds μ)) : Filter.Tendsto (fun (i : γ) => transportCost (fun (z : X × X) => min (edist z.1 z.2) ↑C ^ p.toReal) ↑(μs i) ↑μ) L (nhds 0)

Truncated power costs along weak convergence. On a separable pseudometric space, let probability measures μᵢ converge weakly to μ. Then for every finite nonzero exponent p and every truncation level C, the transport cost of min (edist x y) C ^ p from μᵢ to μ tends to 0.