Documentation

TauCeti.MeasureTheory.OptimalTransport.Wasserstein.LowerSemicontinuous

Lower semicontinuity of the Wasserstein distance under weak convergence #

On a Polish ground space the p-Wasserstein distance is a lower semicontinuous function of the pair of laws for the weak topology on ProbabilityMeasure X × ProbabilityMeasure X: if μₙ ⇀ μ and νₙ ⇀ ν, then

W_p (μ, ν) ≤ liminf W_p (μₙ, νₙ).

The inequality can be strict — for μₙ = (1 - 1 / n) δ₀ + (1 / n) δₙ on ℝ one has μₙ ⇀ δ₀ while W₁ (μₙ, δ₀) = 1 — so weak convergence does not make W_p continuous; that needs the convergence of p-moments as well. Lower semicontinuity is what the direct method consumes whenever a Wasserstein distance appears in a functional to be minimised over weakly compact sets of laws.

For a positive finite exponent the distance is a continuous increasing function of the optimal transport cost of edist ^ p (TauCeti.wassersteinEDist_rpow_eq_transportCost), and that cost is weakly lower semicontinuous in the marginals by TauCeti.lowerSemicontinuous_transportCost; at exponent zero the distance between probability measures vanishes. These arguments need only an extended pseudometric whose topology is Polish. In this same regime the endpoint p = ∞ follows from TauCeti.wassersteinEDist_top_eq_iSup, since a supremum of lower semicontinuous functions is lower semicontinuous.

Main statements #

References #

The Wasserstein distance is weakly lower semicontinuous, for every exponent including p = ∞: on an extended pseudometric space with Polish topology, (μ, ν) ↦ W_p (μ, ν) is lower semicontinuous on ProbabilityMeasure X × ProbabilityMeasure X.

theorem TauCeti.wassersteinEDist_le_liminf {X : Type u_1} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {ι : Type u_2} {l : Filter ι} {μs νs : ι → MeasureTheory.ProbabilityMeasure X} {μ ν : MeasureTheory.ProbabilityMeasure X} (hμ : Filter.Tendsto μs l (nhds μ)) (hν : Filter.Tendsto νs l (nhds ν)) (p : ENNReal) :
wassersteinEDist p ↑μ ↑ν ≤ Filter.liminf (fun (i : ι) => wassersteinEDist p ↑(μs i) ↑(νs i)) l

Weak limits do not increase the Wasserstein distance: on an extended pseudometric space with Polish topology, if μₙ ⇀ μ and νₙ ⇀ ν along a filter l, then W_p (μ, ν) ≤ liminf W_p (μₙ, νₙ) for every exponent p, including p = ∞.

theorem TauCeti.WassersteinSpace.edist_le_liminf {X : Type u_1} [PseudoMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {p : ENNReal} [Fact (1 ≤ p)] {ι : Type u_2} {l : Filter ι} {μ ν : WassersteinSpace p X} {v : ι → WassersteinSpace p X} (h : Filter.Tendsto (fun (i : ι) => ↑(v i)) l (nhds ↑ν)) :
edist μ ν ≤ Filter.liminf (fun (i : ι) => edist μ (v i)) l

Weak limits do not increase the distance from a fixed law of P_p (X): on a pseudometric ground space with Polish topology, if the laws of a family v of P_p (X) converge weakly to the law of ν along a filter l, then W_p (μ, ν) ≤ liminf W_p (μ, v i) for every law μ of P_p (X).