The Wasserstein distance at the infinite exponent

At p = ∞ the Wasserstein distance TauCeti.wassersteinEDist ∞ μ ν is the infimum, over the couplings π of μ and ν, of the π-essential supremum of the ground distance (TauCeti.wassersteinEDist_top). On an extended pseudometric space with Polish topology, this file proves two facts that tie this endpoint to the finite exponents and make it usable:

• the infimum is attained, between any two finite measures that admit a coupling;
• for probability measures, W_∞ (μ, ν) is the supremum of the finite-exponent distances W_p (μ, ν), and it is their limit as p → ∞.

Both are identities in [0, ∞]: no bounded support or moment hypothesis is needed, since a divergent supremum and an infinite W_∞ are allowed on both sides. Monotonicity in the exponent, TauCeti.wassersteinEDist_mono_exponent, makes the supremum over all finite exponents the same as the supremum over 1 ≤ p < ∞.

Main statements

• TauCeti.wassersteinEDist_top_eq_iSup — W_∞ (μ, ν) = ⨆ p < ∞, W_p (μ, ν) when μ is a probability measure;
• TauCeti.tendsto_wassersteinEDist_atTop — W_p (μ, ν) → W_∞ (μ, ν) as p → ∞;
• TauCeti.exists_isCoupling_eLpNorm_top_eq_wassersteinEDist — attainment of the infimum defining W_∞, between finite measures that admit a coupling.

Implementation notes

Monotonicity gives ⨆ p < ∞, W_p ≤ W_∞. For the other inequality, write L for the supremum. The couplings π with ‖d‖_{Lⁿ(π)} ≤ L form a decreasing sequence of nonempty weakly closed subsets of the weakly compact set of couplings: nonempty by attainment at finite exponents, closed because π ↦ ∫⁻ dⁿ ∂π is lower semicontinuous. A coupling in their intersection has all its Lⁿ displacements at most L, hence its essential-supremum displacement is at most L, because the Lⁿ seminorms of a function converge to its essential supremum (TauCeti.tendsto_eLpNorm_atTop). That coupling attains W_∞, which is how attainment and the supremum formula come out of the same argument.

References

• C. R. Givens and R. M. Shortt, A class of Wasserstein metrics for probability distributions, Michigan Math. J. 31 (1984), 231–240, Proposition 1: on a Polish space, W_∞ is the limit of the W_p as p → ∞, and the infimum defining it is attained.

theorem TauCeti.wassersteinEDist_top_eq_iSup {X : Type u_1} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] : wassersteinEDist ⊤ μ ν = ⨆ (p : NNReal), wassersteinEDist (↑p) μ ν

W_∞ is the supremum of the finite-exponent Wasserstein distances. On an extended pseudometric space with Polish topology, if μ is a probability measure then W_∞ (μ, ν) = ⨆ p < ∞, W_p (μ, ν) in [0, ∞]. By monotonicity in the exponent the supremum may equally be taken over 1 ≤ p < ∞.

theorem TauCeti.tendsto_wassersteinEDist_atTop {X : Type u_1} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] : Filter.Tendsto (fun (p : NNReal) => wassersteinEDist (↑p) μ ν) Filter.atTop (nhds (wassersteinEDist ⊤ μ ν))

W_p converges to W_∞. On an extended pseudometric space with Polish topology, if μ is a probability measure then W_p (μ, ν) tends to W_∞ (μ, ν) in [0, ∞] as the exponent p tends to infinity.

theorem TauCeti.exists_isCoupling_eLpNorm_top_eq_wassersteinEDist {X : Type u_1} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (hcoup : ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν) : ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν ∧ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) ⊤ π = wassersteinEDist ⊤ μ ν

Attainment at the infinite exponent. On an extended pseudometric space with Polish topology, the infimum defining W_∞ (μ, ν) between two finite measures that admit a coupling is a minimum: some coupling has essential-supremum displacement exactly W_∞ (μ, ν).

theorem TauCeti.wassersteinEDist_top_le_iff {X : Type u_1} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (hcoup : ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν) {r : ENNReal} : wassersteinEDist ⊤ μ ν ≤ r ↔ ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν ∧ ∀ᵐ (z : X × X) ∂π, edist z.1 z.2 ≤ r

A bound on W_∞ is realized by a coupling whose displacement satisfies that bound almost everywhere. Feasibility is explicit so the statement also holds for the bound ∞.