Wasserstein distance under pushforward

The laws of two a.e. strongly measurable maps can be compared by pushing forward a coupling of their source measures, with no topology on the sources or separability of the target. The radial moment condition transfers exactly between the map and its law.

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_eLpNorm bounds the distance between the laws of two a.e. strongly measurable maps from arbitrary measurable spaces into a Borel extended pseudometric space, using any coupling of their source measures.
• TauCeti.wassersteinEDist_map_le_eLpNorm_of_measurable_edist gives the same bound for a.e. measurable maps into any space with a measurable extended distance, such as ℝ≥0∞, which is not a pseudometric space in its order topology.
• TauCeti.hasFiniteMoment_map_iff_memLp_edist identifies the moment condition on a law with radial MemLp on its source.
• TauCeti.exists_coe_eq_map_of_memLp shows that the law of a map of Lᵖ under a probability measure lies in the finite-moment Wasserstein space.
• 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.isometry_map shows that pushforward by an isometric measurable embedding is an isometry of finite-moment Wasserstein spaces.
• TauCeti.WassersteinSpace.mapIsometryEquiv lifts measurable isometric equivalences.
• TauCeti.wassersteinEDist_map_eq gives invariance under an isometric measurable embedding.
• TauCeti.wassersteinEDist_map_prod_le shows that a common random nonexpansive map does not increase the Wasserstein distance.

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_eLpNorm {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [PseudoEMetricSpace Z] [BorelSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} {f : X → Z} {g : Y → Z} {p : ENNReal} (hπ : IsCoupling π μ ν) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g ν) : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map g ν) ≤ MeasureTheory.eLpNorm (fun (q : X × Y) => edist (f q.1) (g q.2)) p π

Two a.e. strongly measurable maps send a coupling to a transport plan whose cost bounds the Wasserstein distance of their laws. The source spaces need no topology, and the target need not be separable. This holds for every exponent, including ∞, without moment assumptions.

theorem TauCeti.wassersteinEDist_map_le_eLpNorm_of_measurable_edist {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [EDist Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} {f : X → Z} {g : Y → Z} {p : ENNReal} (hπ : IsCoupling π μ ν) (hd : Measurable fun (z : Z × Z) => edist z.1 z.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map g ν) ≤ MeasureTheory.eLpNorm (fun (q : X × Y) => edist (f q.1) (g q.2)) p π

Two a.e. measurable maps into a space with a measurable extended distance send a coupling to a transport plan whose cost bounds the Wasserstein distance of their laws. The target needs no topology, so this applies to ℝ≥0∞, which is not a pseudometric space in its order topology.

theorem TauCeti.hasFiniteMoment_map_iff_memLp_edist {X : Type u_1} {Z : Type u_2} [MeasurableSpace X] [MeasurableSpace Z] [PseudoMetricSpace Z] [OpensMeasurableSpace Z] {μ : MeasureTheory.Measure X} {f : X → Z} {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : AEMeasurable f μ) (z : Z) : HasFiniteMoment p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (fun (x : X) => edist (f x) z) p μ

The law of an a.e. measurable map has finite p-moment exactly when its distance from a specified basepoint belongs to Lᵖ on the source. This also covers the essential-boundedness condition at p = ∞.

theorem TauCeti.exists_coe_eq_map_of_memLp {X : Type u_1} {F : Type u_2} [MeasurableSpace X] [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F] {p : ENNReal} {ν : MeasureTheory.ProbabilityMeasure X} {T : X → F} (hT : MeasureTheory.MemLp T p ↑ν) : ∃ (ν' : WassersteinSpace p F), ↑↑ν' = MeasureTheory.Measure.map T ↑ν

Pushing a law forward by a map of Lᵖ. The law of a map T ∈ Lᵖ(ν; F) under a probability measure ν is a law of finite p-moment, that is, a point of P_p(F).

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.

@[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} {f : X → Y} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (hf : MeasurableEmbedding f) (hi : Isometry f) (μ ν : MeasureTheory.Measure X) : wassersteinEDist p (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) = wassersteinEDist p μ ν

Pushforward by an isometric measurable embedding 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} (he : Isometry ⇑e) : HasFiniteMoment p (MeasureTheory.Measure.map (⇑e) μ) ↔ HasFiniteMoment p μ

A measurable isometric equivalence preserves the finite-moment condition.

theorem TauCeti.wassersteinEDist_map_prod_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {H : Type w} [MeasurableSpace H] (hdX : Measurable fun (z : X × X) => edist z.1 z.2) (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) {f : X × H → Y} (hf : Measurable f) (hfi : ∀ (z : H), LipschitzWith 1 fun (x : X) => f (x, z)) (μ ν : MeasureTheory.Measure X) (η : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure η] : wassersteinEDist p (MeasureTheory.Measure.map f (μ.prod η)) (MeasureTheory.Measure.map f (ν.prod η)) ≤ wassersteinEDist p μ ν

A common random nonexpansive map does not increase the Wasserstein distance. If every section f (·, z) is 1-Lipschitz and η is a probability law, then pushing μ ⊗ η and ν ⊗ η forward along f does not increase the p-Wasserstein distance, for every exponent p.

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.

theorem TauCeti.WassersteinSpace.isometry_map {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {p : ENNReal} {f : X → Y} [PseudoMetricSpace X] [PseudoMetricSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] [BorelSpace X] [BorelSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [Fact (1 ≤ p)] (hf : MeasurableEmbedding f) (hi : Isometry f) : Isometry (map f ⋯ ⋯ ⋯)

Pushforward by an isometric measurable embedding is an isometry 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.

@[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.