Finite-distance Wasserstein spaces

The Wasserstein distance can be infinite, even between probability measures. This file isolates the parts on which it is finite and hence defines an ordinary pseudometric:

• TauCeti.WassersteinComponent p μ₀ consists of the probability measures at finite p-Wasserstein distance from the anchor μ₀;
• TauCeti.WassersteinSpace p X consists of the probability measures on X with finite p-moment.

Every pseudoemetric and pseudometric structure below needs 1 ≤ p, since that is the range in which the Wasserstein triangle inequality holds; the abstract constructors take it as an explicit hypothesis and the instances read it off Fact (1 ≤ p). For such p, on a standard Borel extended pseudometric space with measurable ground distance, every anchored component carries the Wasserstein pseudoemetric, and hence the real-valued Wasserstein pseudometric, because distances inside a single component are finite. On an ordinary pseudometric space, finite moment about one point is equivalent to finite Wasserstein distance from the Dirac mass at any point. Consequently WassersteinSpace p X is canonically equivalent, after choosing a point x₀, to the component anchored at δ_[x₀], and it carries the same Wasserstein pseudometric without a basepoint appearing in its definition. More generally, every finite-moment probability measure anchors exactly the same carrier; this identification is measurable in both directions and is an isometry for the Wasserstein pseudometrics.

When moreover the ground space is Polish and its distance separates points, both pseudometrics are metrics. The measurable structures are the subtype structures inherited from ProbabilityMeasure; no second measurable-space instance is introduced. Identifying these measurable structures with the Borel sigma algebras of the Wasserstein metrics is a separate topological result.

Neither carrier exposes its subtype body: elements are built with TauCeti.WassersteinComponent.mk and TauCeti.WassersteinSpace.mk, and taken apart with toProbabilityMeasure together with TauCeti.WassersteinComponent.wassersteinEDist_anchor_ne_top and TauCeti.WassersteinSpace.hasFiniteMoment. The identification equivComponent leaves the underlying probability measure unchanged, hence is an isometry for the two Wasserstein pseudometrics and is measurable in both directions.

Main definitions

• TauCeti.WassersteinComponent p μ₀ — the finite-distance component of an anchor law;
• TauCeti.WassersteinSpace p X — probability laws with finite p-moment;
• TauCeti.WassersteinSpace.equivComponent — identification with a Dirac-anchored component.
• TauCeti.WassersteinSpace.isometryEquivComponent — the isometric form of that identification.
• TauCeti.WassersteinSpace.measurableEquivComponentOfFiniteMoment — identification with the component of an arbitrary finite-moment anchor;
• TauCeti.WassersteinSpace.isometryEquivComponentOfFiniteMoment — its isometric form.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 6.

def TauCeti.WassersteinComponent {X : Type u} [MeasurableSpace X] [PseudoEMetricSpace X] (p : ENNReal) (μ₀ : MeasureTheory.ProbabilityMeasure X) : Type u

Probability measures at finite p-Wasserstein distance from the anchor μ₀.

This is a type synonym for a subtype, so it can carry the Wasserstein topology independently of the weak topology already present on ProbabilityMeasure. Its measurable structure is still the canonical subtype structure. The subtype body is not exposed: use TauCeti.WassersteinComponent.mk and TauCeti.WassersteinComponent.toProbabilityMeasure.

def TauCeti.WassersteinSpace (p : ENNReal) (X : Type u) [MeasurableSpace X] [PseudoEMetricSpace X] : Type u

Probability measures on X with finite p-moment.

As for TauCeti.WassersteinComponent, the subtype body is not exposed: use TauCeti.WassersteinSpace.mk and TauCeti.WassersteinSpace.toProbabilityMeasure.

noncomputable def TauCeti.WassersteinComponent.mk {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (μ : MeasureTheory.ProbabilityMeasure X) (hμ : wassersteinEDist p ↑μ₀ ↑μ ≠ ⊤) : WassersteinComponent p μ₀

The element of the component anchored at μ₀ given by a probability measure at finite p-Wasserstein distance from μ₀.

noncomputable def TauCeti.WassersteinComponent.toProbabilityMeasure {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (μ : WassersteinComponent p μ₀) : MeasureTheory.ProbabilityMeasure X

The probability measure underlying an element of a Wasserstein component.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinComponent.instCoeOutProbabilityMeasure {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} : CoeOut (WassersteinComponent p μ₀) (MeasureTheory.ProbabilityMeasure X)

theorem TauCeti.WassersteinComponent.toProbabilityMeasure_injective {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} : Function.Injective toProbabilityMeasure

The inclusion of a Wasserstein component into probability measures is injective.

theorem TauCeti.WassersteinComponent.ext {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} {μ ν : WassersteinComponent p μ₀} (h : ↑μ = ↑ν) : μ = ν

Two elements of a Wasserstein component are equal when their probability measures are equal.

theorem TauCeti.WassersteinComponent.ext_iff {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} {μ ν : WassersteinComponent p μ₀} : μ = ν ↔ ↑μ = ↑ν

@[instance_reducible]

noncomputable instance TauCeti.WassersteinComponent.instMeasurableSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} : MeasurableSpace (WassersteinComponent p μ₀)

A Wasserstein component inherits the Giry measurable structure from probability measures.

theorem TauCeti.WassersteinComponent.measurable_toProbabilityMeasure {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} : Measurable toProbabilityMeasure

The inclusion of a Wasserstein component into probability measures is measurable.

@[simp]

theorem TauCeti.WassersteinComponent.coe_mk {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (μ : MeasureTheory.ProbabilityMeasure X) (hμ : wassersteinEDist p ↑μ₀ ↑μ ≠ ⊤) : ↑(mk μ hμ) = μ

theorem TauCeti.WassersteinComponent.measurable_mk {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} {Y : Type u_1} [MeasurableSpace Y] {f : Y → MeasureTheory.ProbabilityMeasure X} (hf : Measurable f) (hmem : ∀ (y : Y), wassersteinEDist p ↑μ₀ ↑(f y) ≠ ⊤) : Measurable fun (y : Y) => mk (f y) ⋯

A measurably varying family of probability measures in an anchored component gives a measurable map into that component.

theorem TauCeti.WassersteinComponent.wassersteinEDist_anchor_ne_top {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (μ : WassersteinComponent p μ₀) : wassersteinEDist p ↑μ₀ ↑↑μ ≠ ⊤

Every element of the component anchored at μ₀ is at finite Wasserstein distance from μ₀; together with TauCeti.WassersteinComponent.mk this characterises the elements of the component.

@[simp]

theorem TauCeti.WassersteinComponent.mk_coe {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (μ : WassersteinComponent p μ₀) : mk ↑μ ⋯ = μ

@[instance_reducible]

noncomputable def TauCeti.WassersteinComponent.pseudoEMetricSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [StandardBorelSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) : PseudoEMetricSpace (WassersteinComponent p μ₀)

The Wasserstein extended distance equips every anchored finite-distance component with a pseudoemetric space structure whenever the ground extended distance is measurable and 1 ≤ p.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinComponent.instPseudoEMetricSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [StandardBorelSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] : PseudoEMetricSpace (WassersteinComponent p μ₀)

The canonical Wasserstein pseudoemetric on an anchored component when the ground extended distance is Borel measurable.

@[simp]

theorem TauCeti.WassersteinComponent.edist_def {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [StandardBorelSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (μ ν : WassersteinComponent p μ₀) : edist μ ν = wassersteinEDist p ↑↑μ ↑↑ν

The extended distance on a Wasserstein component is the Wasserstein distance of the underlying probability measures.

theorem TauCeti.WassersteinComponent.edist_ne_top {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [StandardBorelSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (μ ν : WassersteinComponent p μ₀) : edist μ ν ≠ ⊤

Any two laws in one anchored Wasserstein component are at finite distance from one another.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinComponent.instPseudoMetricSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [StandardBorelSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] : PseudoMetricSpace (WassersteinComponent p μ₀)

Every anchored finite-distance component carries the real-valued Wasserstein pseudometric.

@[simp]

theorem TauCeti.WassersteinComponent.dist_def {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [StandardBorelSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (μ ν : WassersteinComponent p μ₀) : dist μ ν = (wassersteinEDist p ↑↑μ ↑↑ν).toReal

The distance on a Wasserstein component is the real value of the Wasserstein extended distance.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinComponent.instMetricSpace {X : Type u} {p : ENNReal} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [CompleteSpace X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} : MetricSpace (WassersteinComponent p μ₀)

On a Polish metric ground space, Wasserstein distance separates laws, so every anchored finite-distance component is a metric space.

noncomputable def TauCeti.WassersteinSpace.mk {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : MeasureTheory.ProbabilityMeasure X) (hμ : HasFiniteMoment p ↑μ) : WassersteinSpace p X

The element of WassersteinSpace p X given by a probability measure of finite p-moment.

noncomputable def TauCeti.WassersteinSpace.toProbabilityMeasure {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : WassersteinSpace p X) : MeasureTheory.ProbabilityMeasure X

The probability measure underlying an element of WassersteinSpace p X.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinSpace.instCoeOutProbabilityMeasure {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] : CoeOut (WassersteinSpace p X) (MeasureTheory.ProbabilityMeasure X)

theorem TauCeti.WassersteinSpace.toProbabilityMeasure_injective {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] : Function.Injective toProbabilityMeasure

The inclusion of finite-moment laws into probability measures is injective.

theorem TauCeti.WassersteinSpace.ext {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ ν : WassersteinSpace p X} (h : ↑μ = ↑ν) : μ = ν

Two finite-moment laws are equal when their probability measures are equal.

theorem TauCeti.WassersteinSpace.ext_iff {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {μ ν : WassersteinSpace p X} : μ = ν ↔ ↑μ = ↑ν

@[instance_reducible]

noncomputable instance TauCeti.WassersteinSpace.instMeasurableSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] : MeasurableSpace (WassersteinSpace p X)

WassersteinSpace p X inherits the Giry measurable structure from probability measures.

theorem TauCeti.WassersteinSpace.measurable_toProbabilityMeasure {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] : Measurable toProbabilityMeasure

The inclusion of finite-moment laws into probability measures is measurable.

@[simp]

theorem TauCeti.WassersteinSpace.coe_mk {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : MeasureTheory.ProbabilityMeasure X) (hμ : HasFiniteMoment p ↑μ) : ↑(mk μ hμ) = μ

theorem TauCeti.WassersteinSpace.measurable_mk {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] {Y : Type u_1} [MeasurableSpace Y] {f : Y → MeasureTheory.ProbabilityMeasure X} (hf : Measurable f) (hmem : ∀ (y : Y), HasFiniteMoment p ↑(f y)) : Measurable fun (y : Y) => mk (f y) ⋯

A measurably varying family of finite-moment probability measures gives a measurable map into the Wasserstein space.

theorem TauCeti.WassersteinSpace.hasFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : WassersteinSpace p X) : HasFiniteMoment p ↑↑μ

Every law in WassersteinSpace p X has finite p-moment; together with TauCeti.WassersteinSpace.mk this characterises its elements.

@[simp]

theorem TauCeti.WassersteinSpace.mk_coe {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : WassersteinSpace p X) : mk ↑μ ⋯ = μ

theorem TauCeti.WassersteinSpace.isEmpty_of_isEmpty {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoEMetricSpace X] [IsEmpty X] : IsEmpty (WassersteinSpace p X)

The Wasserstein space over an empty ground space is empty: there is no probability measure.

noncomputable def TauCeti.WassersteinSpace.equivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [BorelSpace X] [SecondCountableTopology X] (x₀ : X) : WassersteinSpace p X ≃ WassersteinComponent p (MeasureTheory.diracProba x₀)

Choosing a basepoint identifies the finite-moment Wasserstein space with the finite-distance component anchored at its Dirac law. The underlying probability measure is unchanged.

@[simp]

theorem TauCeti.WassersteinSpace.coe_equivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [BorelSpace X] [SecondCountableTopology X] (x₀ : X) (μ : WassersteinSpace p X) : ↑((equivComponent x₀) μ) = ↑μ

@[simp]

theorem TauCeti.WassersteinSpace.coe_equivComponent_symm {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [BorelSpace X] [SecondCountableTopology X] (x₀ : X) (μ : WassersteinComponent p (MeasureTheory.diracProba x₀)) : ↑((equivComponent x₀).symm μ) = ↑μ

theorem TauCeti.WassersteinSpace.measurable_equivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [BorelSpace X] [SecondCountableTopology X] (x₀ : X) : Measurable ⇑(equivComponent x₀)

The identification with a Dirac-anchored component is measurable: it does not change the underlying probability measure, and both sides carry the subtype measurable structure.

theorem TauCeti.WassersteinSpace.measurable_equivComponent_symm {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [BorelSpace X] [SecondCountableTopology X] (x₀ : X) : Measurable ⇑(equivComponent x₀).symm

The inverse of the identification with a Dirac-anchored component is measurable.

noncomputable def TauCeti.WassersteinSpace.measurableEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hμ₀ : HasFiniteMoment p ↑μ₀) : WassersteinSpace p X ≃ᵐ WassersteinComponent p μ₀

A finite-moment anchor identifies the usual finite-moment Wasserstein space with its finite-distance component. The equivalence leaves the underlying probability measure unchanged, hence is measurable in both directions: both carriers inherit the measurable structure of ProbabilityMeasure.

@[simp]

theorem TauCeti.WassersteinSpace.coe_measurableEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hμ₀ : HasFiniteMoment p ↑μ₀) (μ : WassersteinSpace p X) : ↑((measurableEquivComponentOfFiniteMoment hd hμ₀) μ) = ↑μ

@[simp]

theorem TauCeti.WassersteinSpace.coe_measurableEquivComponentOfFiniteMoment_symm {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hμ₀ : HasFiniteMoment p ↑μ₀) (μ : WassersteinComponent p μ₀) : ↑((measurableEquivComponentOfFiniteMoment hd hμ₀).symm μ) = ↑μ

theorem TauCeti.WassersteinSpace.wassersteinEDist_ne_top {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (μ ν : WassersteinSpace p X) : wassersteinEDist p ↑↑μ ↑↑ν ≠ ⊤

Two finite-moment laws are at finite Wasserstein distance: this is the general finite-moment anchor criterion with the source law as the anchor.

theorem TauCeti.WassersteinSpace.exists_coe_eq_smul_add_smul {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [OpensMeasurableSpace X] {a b : ENNReal} (hab : a + b = 1) (μ ν : WassersteinSpace p X) : ∃ (ρ : WassersteinSpace p X), ↑↑ρ = a • ↑↑μ + b • ↑↑ν

P_p(X) is convex. For weights with a + b = 1, the mixture a • μ + b • ν of two laws of P_p(X) is again a law of P_p(X).

theorem TauCeti.WassersteinSpace.exists_coe_eq_cond {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [OpensMeasurableSpace X] {m : MeasureTheory.Measure X} {s : Set X} (hs : MeasurableSet s) (hb : Bornology.IsBounded s) (h₀ : m s ≠ 0) (hfin : m s ≠ ⊤) : ∃ (μ : WassersteinSpace p X), ↑↑μ = m[|s] ∧ Bornology.IsBounded (↑↑μ).support ∧ (↑↑μ).AbsolutelyContinuous m

Uniform laws on bounded sets lie in P_p(X). The normalised restriction m[|s] of a measure m to a bounded measurable set s of positive, finite measure is a law of P_p(X). It is carried by s, so it has bounded support and is absolutely continuous with respect to m.

theorem TauCeti.WassersteinSpace.sum_mul_wassersteinEDist_rpow_ne_top {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [BorelSpace X] [SecondCountableTopology X] {J : Type u_1} [Fintype J] {w : J → NNReal} (μ : J → WassersteinSpace p X) (z : WassersteinSpace p X) : ∑ j : J, ↑(w j) * wassersteinEDist p ↑↑z ↑↑(μ j) ^ p.toReal ≠ ⊤

The weighted p-Wasserstein cost against finitely many points of P_p(X) is finite at every point of P_p(X).

@[instance_reducible]

noncomputable def TauCeti.WassersteinSpace.pseudoEMetricSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) : PseudoEMetricSpace (WassersteinSpace p X)

The Wasserstein extended distance equips finite-moment laws with a pseudoemetric space structure whenever the ground distance is measurable and 1 ≤ p.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinSpace.instPseudoEMetricSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] : PseudoEMetricSpace (WassersteinSpace p X)

The canonical Wasserstein pseudoemetric on finite-moment laws when the ground distance is Borel measurable.

@[simp]

theorem TauCeti.WassersteinSpace.edist_def {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (μ ν : WassersteinSpace p X) : edist μ ν = wassersteinEDist p ↑↑μ ↑↑ν

The extended distance on finite-moment laws is their Wasserstein distance.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinSpace.instPseudoMetricSpace {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] : PseudoMetricSpace (WassersteinSpace p X)

Finite-moment laws carry the real-valued Wasserstein pseudometric.

@[simp]

theorem TauCeti.WassersteinSpace.dist_def {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (μ ν : WassersteinSpace p X) : dist μ ν = (wassersteinEDist p ↑↑μ ↑↑ν).toReal

The distance on finite-moment laws is the real value of the Wasserstein extended distance.

theorem TauCeti.WassersteinSpace.edist_equivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (x₀ : X) (μ ν : WassersteinSpace p X) : edist ((equivComponent x₀) μ) ((equivComponent x₀) ν) = edist μ ν

The identification with a Dirac-anchored component preserves the Wasserstein extended distance, since it does not change the underlying probability measure.

theorem TauCeti.WassersteinSpace.isometry_equivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (x₀ : X) : Isometry ⇑(equivComponent x₀)

Choosing a basepoint identifies WassersteinSpace p X isometrically with the finite-distance component anchored at the Dirac law of that basepoint.

noncomputable def TauCeti.WassersteinSpace.isometryEquivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (x₀ : X) : WassersteinSpace p X ≃ᵢ WassersteinComponent p (MeasureTheory.diracProba x₀)

Choosing a basepoint gives an isometric equivalence from WassersteinSpace p X to the finite-distance component anchored at the Dirac law of that basepoint.

theorem TauCeti.WassersteinSpace.dist_equivComponent {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (x₀ : X) (μ ν : WassersteinSpace p X) : dist ((equivComponent x₀) μ) ((equivComponent x₀) ν) = dist μ ν

The identification with a Dirac-anchored component preserves the real-valued Wasserstein distance.

theorem TauCeti.WassersteinSpace.edist_measurableEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hμ₀ : HasFiniteMoment p ↑μ₀) (μ ν : WassersteinSpace p X) : edist ((measurableEquivComponentOfFiniteMoment ⋯ hμ₀) μ) ((measurableEquivComponentOfFiniteMoment ⋯ hμ₀) ν) = edist μ ν

The identification with a finite-moment anchored component preserves the Wasserstein extended distance.

theorem TauCeti.WassersteinSpace.isometry_measurableEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hμ₀ : HasFiniteMoment p ↑μ₀) : Isometry ⇑(measurableEquivComponentOfFiniteMoment ⋯ hμ₀)

The identification with a finite-moment anchored component is an isometry.

noncomputable def TauCeti.WassersteinSpace.isometryEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hμ₀ : HasFiniteMoment p ↑μ₀) : WassersteinSpace p X ≃ᵢ WassersteinComponent p μ₀

A finite-moment anchor gives an isometric equivalence from P_p(X) to its finite-distance component.

@[simp]

theorem TauCeti.WassersteinSpace.coe_isometryEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hμ₀ : HasFiniteMoment p ↑μ₀) (μ : WassersteinSpace p X) : ↑((isometryEquivComponentOfFiniteMoment hμ₀) μ) = ↑μ

@[simp]

theorem TauCeti.WassersteinSpace.coe_isometryEquivComponentOfFiniteMoment_symm {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hμ₀ : HasFiniteMoment p ↑μ₀) (μ : WassersteinComponent p μ₀) : ↑((isometryEquivComponentOfFiniteMoment hμ₀).symm μ) = ↑μ

theorem TauCeti.WassersteinSpace.dist_measurableEquivComponentOfFiniteMoment {X : Type u} {p : ENNReal} [MeasurableSpace X] [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] {μ₀ : MeasureTheory.ProbabilityMeasure X} (hμ₀ : HasFiniteMoment p ↑μ₀) (μ ν : WassersteinSpace p X) : dist ((measurableEquivComponentOfFiniteMoment ⋯ hμ₀) μ) ((measurableEquivComponentOfFiniteMoment ⋯ hμ₀) ν) = dist μ ν

The finite-moment-anchor identification preserves the real-valued Wasserstein distance.

@[instance_reducible]

noncomputable instance TauCeti.WassersteinSpace.instMetricSpace {X : Type u} {p : ENNReal} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [CompleteSpace X] [Fact (1 ≤ p)] : MetricSpace (WassersteinSpace p X)

On a Polish metric ground space, the Wasserstein pseudometric on finite-moment laws is a metric.

theorem TauCeti.transportCost_norm_sub_sq_div_two_ne_top {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ ν : WassersteinSpace 2 E) : transportCost (fun (z : E × E) => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) ↑↑μ ↑↑ν ≠ ⊤

Laws with finite second moment have finite transport cost for ‖x - y‖ ^ 2 / 2: the cost is at most ‖x - y‖ ^ 2, whose transport cost is the square of their finite 2-Wasserstein distance.

theorem TauCeti.WassersteinSpace.dist_sq_le_integral {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {ν₀ ν₁ : WassersteinSpace 2 E} {π : MeasureTheory.Measure (E × E)} (hπ : IsCoupling π ↑↑ν₀ ↑↑ν₁) : dist ν₀ ν₁ ^ 2 ≤ ∫ (z : E × E), ‖z.1 - z.2‖ ^ 2 ∂π

The squared quadratic Wasserstein distance between two laws of P₂(E) is at most the quadratic cost ∫ ‖x - y‖² dπ of any of their couplings π.

theorem TauCeti.WassersteinSpace.dist_sq_eq_integral {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {ν₀ ν₁ : WassersteinSpace 2 E} {π : MeasureTheory.Measure (E × E)} (hπ : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ 2) π ↑↑ν₀ ↑↑ν₁) : dist ν₀ ν₁ ^ 2 = ∫ (z : E × E), ‖z.1 - z.2‖ ^ 2 ∂π

An optimal coupling π of two laws of P₂(E) for the quadratic cost realizes their squared quadratic Wasserstein distance as its quadratic cost: dist ν₀ ν₁ ^ 2 = ∫ ‖x - y‖² dπ.

theorem TauCeti.WassersteinSpace.isOptimalCoupling_of_integral_le_dist_sq {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {ν₀ ν₁ : WassersteinSpace 2 E} {π : MeasureTheory.Measure (E × E)} (hπ : IsCoupling π ↑↑ν₀ ↑↑ν₁) (h : ∫ (z : E × E), ‖z.1 - z.2‖ ^ 2 ∂π ≤ dist ν₀ ν₁ ^ 2) : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ 2) π ↑↑ν₀ ↑↑ν₁

A coupling π of two laws of P₂(E) whose quadratic cost ∫ ‖x - y‖² dπ is at most their squared quadratic Wasserstein distance is an optimal coupling for the quadratic cost. This is the converse of TauCeti.WassersteinSpace.dist_sq_eq_integral.

theorem TauCeti.WassersteinSpace.norm_toLp_sub_eq_dist {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {ν₀ ν₁ : WassersteinSpace 2 E} {π : MeasureTheory.Measure (E × E)} (hπ : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ 2) π ↑↑ν₀ ↑↑ν₁) (hd : MeasureTheory.MemLp (fun (z : E × E) => z.2 - z.1) 2 π) : ‖MeasureTheory.MemLp.toLp (fun (z : E × E) => z.2 - z.1) hd‖ = dist ν₀ ν₁

The L²(π) norm of the displacement (x, y) ↦ y - x of an optimal coupling π of two laws of P₂(E) for the quadratic cost is their quadratic Wasserstein distance.