Wasserstein distance under pushforward

A Lipschitz map sends every coupling to a coupling of the pushforward measures, while increasing the displacement of each coupled pair by at most its Lipschitz constant. Consequently pushforward is Lipschitz for every Wasserstein exponent, including the essential-supremum endpoint.

This file proves the estimate first for the objective of a specified coupling and then for the infimum over all couplings. The latter needs no hypothesis on the measures once the Lipschitz constant is nonzero; for a zero constant it is stated for measures known to admit a coupling, a condition the probability-measure specialization discharges with the independent coupling. It also records preservation of finite moments, so the same map acts on finite-moment Wasserstein spaces.

Main statements

• TauCeti.wassersteinEDist_map_le_mul_eLpNorm bounds the Wasserstein distance of two pushforwards by the Lipschitz constant times the objective of a specified source coupling.
• TauCeti.wassersteinEDist_map_le_mul_of_ne_zero gives the pushforward estimate for arbitrary measures and a nonzero Lipschitz constant.
• TauCeti.wassersteinEDist_map_le_mul_of_exists_isCoupling gives the pushforward estimate for any two measures admitting a coupling.
• TauCeti.wassersteinEDist_map_le_mul is the probability-measure specialization.
• TauCeti.HasFiniteMoment.map shows that Lipschitz pushforward preserves finite moments.
• TauCeti.WassersteinSpace.map lifts pushforward to finite-moment probability measures.
• TauCeti.WassersteinSpace.lipschitzWith_map gives the induced Lipschitz map between Wasserstein spaces.
• TauCeti.WassersteinSpace.mapIsometryEquiv lifts measurable isometric equivalences.
• TauCeti.wassersteinEDist_map_eq gives invariance under a measurable isometric equivalence.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 6.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §5.1.

theorem TauCeti.wassersteinEDist_map_le_mul_eLpNorm {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} {μ ν : MeasureTheory.Measure X} {π : MeasureTheory.Measure (X × X)} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) (hf : Measurable f) (hLip : LipschitzWith K f) (hπ : IsCoupling π μ ν) : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ ↑K * MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π

The image of a specified coupling under a Lipschitz map bounds the Wasserstein distance of the pushforward measures. This is the coupling-level estimate from which functoriality follows.

theorem TauCeti.wassersteinEDist_map_le_mul_of_ne_zero {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) (hf : Measurable f) (hLip : LipschitzWith K f) (hK : K ≠ 0) (μ ν : MeasureTheory.Measure X) : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ ↑K * wassersteinEDist p μ ν

A Lipschitz map contracts Wasserstein distance up to a nonzero Lipschitz constant, for arbitrary measures. Nothing is assumed about μ and ν: if they admit no coupling their distance is ⊤, and multiplying by a nonzero constant leaves the bound at ⊤.

theorem TauCeti.wassersteinEDist_map_le_mul_of_exists_isCoupling {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} {μ ν : MeasureTheory.Measure X} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) (hf : Measurable f) (hLip : LipschitzWith K f) (hμν : ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν) : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ ↑K * wassersteinEDist p μ ν

A Lipschitz map contracts Wasserstein distance up to its Lipschitz constant, for arbitrary measures admitting a coupling. The existence hypothesis is needed only when the Lipschitz constant is zero: with Mathlib's extended-nonnegative-real convention, 0 * ∞ = 0, whereas measures of unequal mass have no coupling and remain at infinite distance after pushforward.

theorem TauCeti.wassersteinEDist_map_le_mul {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) (hf : Measurable f) (hLip : LipschitzWith K f) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ ↑K * wassersteinEDist p μ ν

Pushforward by a K-Lipschitz measurable map is K-Lipschitz for the p-Wasserstein distance between probability measures. The statement includes K = 0, p = 0, and p = ∞.

theorem TauCeti.HasFiniteMoment.map {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} {μ : MeasureTheory.Measure X} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (hμ : HasFiniteMoment p μ) (hdY : ∀ (y : Y), Measurable fun (z : Y) => edist y z) (hf : Measurable f) (hLip : LipschitzWith K f) : HasFiniteMoment p (MeasureTheory.Measure.map f μ)

A Lipschitz measurable map sends a measure with finite p-moment to another measure with finite p-moment.

noncomputable def TauCeti.WassersteinSpace.map {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (f : X → Y) (hdY : ∀ (y : Y), Measurable fun (z : Y) => edist y z) (hf : Measurable f) (hLip : LipschitzWith K f) (mu : WassersteinSpace p X) : WassersteinSpace p Y

Pushforward by a measurable Lipschitz map, as a map between finite-moment Wasserstein spaces.

Equations

• TauCeti.WassersteinSpace.map f hdY hf hLip mu = TauCeti.WassersteinSpace.mk ((↑mu).map f) ⋯

@[simp]

theorem TauCeti.WassersteinSpace.coe_map {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (f : X → Y) (hdY : ∀ (y : Y), Measurable fun (z : Y) => edist y z) (hf : Measurable f) (hLip : LipschitzWith K f) (mu : WassersteinSpace p X) : ↑(map f hdY hf hLip mu) = (↑mu).map f

The probability measure underlying a Wasserstein-space pushforward is the pushforward of the underlying probability measure.

@[simp]

theorem TauCeti.WassersteinSpace.map_id {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoEMetricSpace X] (hdX : ∀ (x : X), Measurable fun (z : X) => edist x z) (mu : WassersteinSpace p X) : map id hdX ⋯ ⋯ mu = mu

Pushforward by the identity map is the identity on finite-moment Wasserstein spaces.

@[simp]

theorem TauCeti.WassersteinSpace.map_map {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {Z : Type w} [MeasurableSpace Z] [PseudoEMetricSpace Z] {g : Y → Z} {K' : NNReal} (hdY : ∀ (y : Y), Measurable fun (z : Y) => edist y z) (hdZ : ∀ (z : Z), Measurable fun (w : Z) => edist z w) (hf : Measurable f) (hLip : LipschitzWith K f) (hg : Measurable g) (hgLip : LipschitzWith K' g) (mu : WassersteinSpace p X) : map g hdZ hg hgLip (map f hdY hf hLip mu) = map (g ∘ f) hdZ ⋯ ⋯ mu

Successive pushforwards are the pushforward along the composition, matching the orientation of MeasureTheory.Measure.map_map.

@[simp]

theorem TauCeti.wassersteinEDist_map_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e : X ≃ᵐ Y} (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) (he : Isometry ⇑e) (μ ν : MeasureTheory.Measure X) : wassersteinEDist p (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑e) ν) = wassersteinEDist p μ ν

A measurable isometric equivalence preserves Wasserstein distance.

@[simp]

theorem TauCeti.hasFiniteMoment_map_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {μ : MeasureTheory.Measure X} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e : X ≃ᵐ Y} (hdY : ∀ (y : Y), Measurable fun (z : Y) => edist y z) (he : Isometry ⇑e) : HasFiniteMoment p (MeasureTheory.Measure.map (⇑e) μ) ↔ HasFiniteMoment p μ

A measurable isometric equivalence preserves the finite-moment condition.

theorem TauCeti.WassersteinSpace.lipschitzWith_map {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {K : NNReal} {f : X → Y} [PseudoMetricSpace X] [PseudoMetricSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] [BorelSpace X] [BorelSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [Fact (1 ≤ p)] (hf : Measurable f) (hLip : LipschitzWith K f) : LipschitzWith K (map f ⋯ hf hLip)

Pushforward by a measurable K-Lipschitz map is K-Lipschitz between finite-moment Wasserstein spaces.

noncomputable def TauCeti.WassersteinSpace.mapIsometryEquiv {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} [PseudoMetricSpace X] [PseudoMetricSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] [BorelSpace X] [BorelSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [Fact (1 ≤ p)] (e : X ≃ᵐ Y) (he : Isometry ⇑e) : WassersteinSpace p X ≃ᵢ WassersteinSpace p Y

A measurable isometric equivalence of ground spaces induces an isometric equivalence of their finite-moment Wasserstein spaces.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.WassersteinSpace.mapIsometryEquiv_apply {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} [PseudoMetricSpace X] [PseudoMetricSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] [BorelSpace X] [BorelSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [Fact (1 ≤ p)] (e : X ≃ᵐ Y) (he : Isometry ⇑e) (mu : WassersteinSpace p X) : (mapIsometryEquiv e he) mu = map ⇑e ⋯ ⋯ ⋯ mu

The isometric equivalence induced by a measurable isometric equivalence acts by pushforward along that equivalence.

@[simp]

theorem TauCeti.WassersteinSpace.mapIsometryEquiv_symm_apply {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} [PseudoMetricSpace X] [PseudoMetricSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] [BorelSpace X] [BorelSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [Fact (1 ≤ p)] (e : X ≃ᵐ Y) (he : Isometry ⇑e) (nu : WassersteinSpace p Y) : (mapIsometryEquiv e he).symm nu = map ⇑e.symm ⋯ ⋯ ⋯ nu

The inverse of the induced isometric equivalence acts by pushforward along the inverse equivalence.