Relatively compact sets of the Wasserstein space

For a finite exponent 1 ≤ p < ∞ and a complete separable metric ground space X, a set S of laws with finite p-moment is relatively compact in the Wasserstein space TauCeti.WassersteinSpace p X exactly when

• it is tight, and
• its p-moments about a basepoint x have uniformly small tails: for every ε > 0 there is a radius R with ∫⁻ y in {y | R ≤ dist x y}, dist x y ^ p ∂μ ≤ ε for every μ ∈ S.

It is compact exactly when it is moreover closed. This is the compactness half of the description of the W_p topology as weak convergence together with uniform integrability of p-moments, whose convergence half is TauCeti.WassersteinSpace.tendsto_iff_tendsto_toProbabilityMeasure_and_lintegral. The criterion does not depend on the basepoint, since the equivalence holds for each one.

The corresponding weak compactness criterion is Mathlib's Prokhorov theorem, stated in MeasureTheory.isTightMeasureSet_of_isCompact_closure and MeasureTheory.isCompact_closure_of_isTightMeasureSet.

Bounded sets of P_p (X) need not be relatively compact, even when X = ℝ, but they keep a narrow form of compactness. By Markov's inequality, bounded sets are tight on a proper space. By Prokhorov's theorem, a bounded tight sequence has a narrowly convergent subsequence, whose narrow limit still has finite p-moment by narrow lower semicontinuity of the Wasserstein distance. This is the compactness used by the direct method in the Wasserstein space.

Main statements

All the following declarations are in the TauCeti namespace.

• WassersteinSpace.isCompact_closure_of_isTightMeasureSet_of_exists_setLIntegral_edist_rpow_le — a tight set with uniformly small p-moment tails is relatively compact, on a separable metric space;
• WassersteinSpace.isTightMeasureSet_of_isCompact_closure — a relatively compact set is tight, on a complete separable pseudometric space;
• WassersteinSpace.exists_setLIntegral_edist_rpow_le_of_isCompact_closure — a relatively compact set has uniformly small p-moment tails about every basepoint;
• WassersteinSpace.isCompact_closure_iff_isTightMeasureSet_and_exists_setLIntegral_edist_rpow_le, WassersteinSpace.isCompact_iff_isClosed_isTightMeasureSet_and_exists_setLIntegral_edist_rpow_le — the resulting characterizations of relatively compact and of compact sets;
• ofReal_mul_measure_compl_closedBall_le_wassersteinEDist — Markov's inequality for the Wasserstein distance from a Dirac law;
• WassersteinSpace.isTightMeasureSet_of_isBounded — on a proper space, bounded sets of P_p (X) are tight;
• WassersteinSpace.isTightMeasureSet_of_exists_setLIntegral_edist_rpow_le and WassersteinSpace.isCompact_closure_iff_exists_setLIntegral_edist_rpow_le — on a proper space, uniformly small p-moment tails imply tightness, so they alone characterize relatively compact sets of P_p (X);
• WassersteinSpace.hasFiniteMoment_of_isBounded_of_tendsto — a narrow limit of a bounded family of P_p (X) has finite p-moment;
• WassersteinSpace.exists_strictMono_tendsto_of_isBounded_of_isTightMeasureSet — a bounded tight sequence of P_p (X) has a subsequence converging narrowly to a law of P_p (X).

References

• L. Ambrosio, N. Gigli and G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd edition, Birkhäuser 2008, §7.1.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 6.

theorem TauCeti.ofReal_mul_measure_compl_closedBall_le_wassersteinEDist {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (x : X) (μ : MeasureTheory.ProbabilityMeasure X) (r : ℝ) : ENNReal.ofReal r * ↑μ (Metric.closedBall x r)ᶜ ≤ wassersteinEDist p (MeasureTheory.Measure.dirac x) ↑μ

Markov's inequality for the Wasserstein distance from a Dirac law. For a probability measure μ and a radius r, the mass of μ outside the closed ball of radius r about x, multiplied by r, is at most W_p (δ_x, μ), for every exponent 1 ≤ p.

theorem TauCeti.WassersteinSpace.isTightMeasureSet_of_isCompact_closure {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] [CompleteSpace X] {S : Set (WassersteinSpace p X)} (hS : IsCompact (closure S)) : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ S, ↑↑μ = x}

A relatively compact set of the Wasserstein space is tight. On a complete separable pseudometric space, the laws of a relatively compact set of P_p (X) form a tight family.

theorem TauCeti.WassersteinSpace.exists_setLIntegral_edist_rpow_le_of_isCompact_closure {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) {S : Set (WassersteinSpace p X)} (hS : IsCompact (closure S)) (x : X) {ε : ENNReal} (hε : 0 < ε) : ∃ (R : NNReal), ∀ μ ∈ S, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑μ ≤ ε

A relatively compact set of the Wasserstein space has uniformly integrable moments. For a finite exponent 1 ≤ p < ∞, the p-moments about any basepoint of the laws of a relatively compact set of P_p (X) have uniformly small tails: for every ε > 0 there is a radius R such that, for every law of the set, the part of its p-moment coming from distance at least R is at most ε.

theorem TauCeti.WassersteinSpace.isCompact_closure_of_isTightMeasureSet_of_exists_setLIntegral_edist_rpow_le {X : Type u_1} {p : ENNReal} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : X) {S : Set (WassersteinSpace p X)} (hT : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ S, ↑↑μ = x}) (hU : ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ μ ∈ S, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑μ ≤ ε) : IsCompact (closure S)

Tightness and uniformly integrable moments give relative compactness. On a separable metric space and for a finite exponent 1 ≤ p < ∞, a set of laws of finite p-moment is relatively compact in P_p (X) as soon as it is tight and its p-moments about a basepoint x have uniformly small tails: for every ε > 0 there is a radius R such that, for every law of the set, the part of its p-moment coming from distance at least R is at most ε.

theorem TauCeti.WassersteinSpace.isCompact_closure_iff_isTightMeasureSet_and_exists_setLIntegral_edist_rpow_le {X : Type u_1} {p : ENNReal} [MetricSpace X] [CompleteSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : X) {S : Set (WassersteinSpace p X)} : IsCompact (closure S) ↔ MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ S, ↑↑μ = x} ∧ ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ μ ∈ S, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑μ ≤ ε

Relatively compact sets of the Wasserstein space. On a complete separable metric space and for a finite exponent 1 ≤ p < ∞, a set of laws of finite p-moment is relatively compact in P_p (X) exactly when it is tight and its p-moments about a basepoint x have uniformly small tails.

theorem TauCeti.WassersteinSpace.isCompact_iff_isClosed_isTightMeasureSet_and_exists_setLIntegral_edist_rpow_le {X : Type u_1} {p : ENNReal} [MetricSpace X] [CompleteSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : X) {S : Set (WassersteinSpace p X)} : IsCompact S ↔ IsClosed S ∧ MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ S, ↑↑μ = x} ∧ ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ μ ∈ S, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑μ ≤ ε

Compact sets of the Wasserstein space. On a complete separable metric space and for a finite exponent 1 ≤ p < ∞, a set of laws of finite p-moment is compact in P_p (X) exactly when it is closed, tight, and its p-moments about a basepoint x have uniformly small tails.

theorem TauCeti.WassersteinSpace.isTightMeasureSet_of_isBounded {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] [StandardBorelSpace X] [ProperSpace X] {S : Set (WassersteinSpace p X)} (hS : Bornology.IsBounded S) : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ S, ↑↑μ = x}

Bounded sets of the Wasserstein space are tight on a proper space. On a proper pseudometric space, the laws of a bounded set of P_p (X) form a tight family: by Markov's inequality, the mass of a law μ outside the closed ball of radius r > 0 about x is at most W_p (δ_x, μ) / r. Bounded sets of P_p (X) need not be relatively compact in P_p (X), whose compact sets also have uniformly integrable p-moments.

theorem TauCeti.WassersteinSpace.isTightMeasureSet_of_exists_setLIntegral_edist_rpow_le {X : Type u_1} {p : ENNReal} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [ProperSpace X] (x : X) {S : Set (WassersteinSpace p X)} (hU : ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ μ ∈ S, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑μ ≤ ε) : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ S, ↑↑μ = x}

Uniformly small moment tails give tightness on a proper space. On a proper pseudometric space, if the p-moments about x of a set of laws of P_p (X) have uniformly small tails, then the laws form a tight family: outside the closed ball of radius r ≥ 1 about x, the mass of a law is at most the part of its p-moment coming from distance at least r.

theorem TauCeti.WassersteinSpace.isCompact_closure_iff_exists_setLIntegral_edist_rpow_le {X : Type u_1} {p : ENNReal} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [ProperSpace X] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : X) {S : Set (WassersteinSpace p X)} : IsCompact (closure S) ↔ ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ μ ∈ S, ∫⁻ (y : X) in {y : X | R ≤ nndist x y}, edist x y ^ p.toReal ∂↑↑μ ≤ ε

Relatively compact sets of the Wasserstein space of a proper space. On a proper metric space and for a finite exponent 1 ≤ p < ∞, a set of laws of finite p-moment is relatively compact in P_p (X) exactly when its p-moments about a basepoint x have uniformly small tails; tightness is then automatic.

theorem TauCeti.WassersteinSpace.hasFiniteMoment_of_isBounded_of_tendsto {X : Type u_1} {p : ENNReal} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [CompleteSpace X] [Fact (1 ≤ p)] {ι : Type u_2} {l : Filter ι} [l.NeBot] {v : ι → WassersteinSpace p X} (hv : Bornology.IsBounded (Set.range v)) {ν : MeasureTheory.ProbabilityMeasure X} (h : Filter.Tendsto (fun (i : ι) => ↑(v i)) l (nhds ν)) : HasFiniteMoment p ↑ν

Narrow limits of bounded families have finite moment. On a complete separable metric space, if a bounded family of laws of P_p (X) converges narrowly to a probability measure ν, then ν has finite p-moment: its Wasserstein distance from any law of the family is at most the diameter of the family, by narrow lower semicontinuity of the Wasserstein distance.

theorem TauCeti.WassersteinSpace.exists_strictMono_tendsto_of_isBounded_of_isTightMeasureSet {X : Type u_1} {p : ENNReal} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [CompleteSpace X] [Fact (1 ≤ p)] {v : ℕ → WassersteinSpace p X} (hv : Bornology.IsBounded (Set.range v)) (htight : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure X | ∃ μ ∈ Set.range v, ↑↑μ = x}) : ∃ (ν : WassersteinSpace p X) (ψ : ℕ → ℕ), StrictMono ψ ∧ Filter.Tendsto (fun (n : ℕ) => ↑(v (ψ n))) Filter.atTop (nhds ↑ν)

Narrow compactness of bounded tight sequences. On a complete separable metric space, a bounded sequence of P_p (X) whose laws form a tight family has a subsequence that converges narrowly to a law of P_p (X). Prokhorov's theorem gives the narrow limit and TauCeti.WassersteinSpace.hasFiniteMoment_of_isBounded_of_tendsto its finite moment. The subsequence need not converge in P_p (X).