The Wasserstein distance of two measures

For an exponent p : ℝ≥0∞ the p-Wasserstein distance of two measures μ and ν on a common space carrying an extended distance is

W_p (μ, ν) = ⨅ π, eLpNorm (fun z ↦ edist z.1 z.2) p π,

the infimum taken over the couplings π of μ and ν. This file defines TauCeti.wassersteinEDist and proves the identities that make it a distance: it vanishes on the diagonal, it is symmetric, it is monotone in the exponent, it satisfies the triangle inequality, and — on a Polish space with a compatible extended pseudometric, where the infimum is attained — it separates measures.

Writing the objective as an eLpNorm rather than as a root of an integral is what makes the exponent p = ∞ a case of the definition instead of a separate one: at that endpoint the value is the infimum of the coupling-wise essential suprema of the ground distance. For 1 ≤ p < ∞ the two readings agree, and TauCeti.wassersteinEDist_rpow_eq_transportCost is the exact bridge to the primal Kantorovich problem of TauCeti.transportCost for the cost edist ^ p.

The two-variable transport identities below assume joint measurability of the ground extended distance, Measurable fun z : X × X ↦ edist z.1 z.2. This is not automatic for an abstract WeakPseudoEMetricSpace sitting on an unrelated measurable space, and it is exactly what is needed to move the objective along a pushforward. When the topology is induced by the ground distance, Mathlib's measurable_edist supplies this on a second countable Borel space. The same hypothesis is what makes the objective computable at all, since MeasureTheory.eLpNorm is ∞ for a function that is not almost-everywhere strongly measurable: that is why the two endpoint readings at p = 0 and p = ∞ and the transport-cost bridge ask for it, even though no pushforward is involved. The pure finite-moment results use only almost-everywhere strong measurability of the relevant distance sections, the two-Dirac value needs no measurability at all, and the vanishing on the diagonal needs only a measurable diagonal, MeasurableEq. The algebraic laws use WeakPseudoEMetricSpace, so the ground distance need not induce the ambient topology. The triangle inequality additionally asks for a standard Borel measurable structure, which is what the gluing lemma consumes.

Main definitions

• TauCeti.wassersteinEDist p μ ν — the infimum of eLpNorm (fun z ↦ edist z.1 z.2) p π over the couplings π of μ and ν.
• TauCeti.HasFiniteMoment p μ — the MemLp finite-moment condition about some basepoint, with TauCeti.hasFiniteMoment_of_ae_mem_finset, TauCeti.hasFiniteMoment_of_ae_mem_of_isBounded, TauCeti.hasFiniteMoment_of_boundedSpace, and TauCeti.hasFiniteMoment_dirac supplying finite moments for finite carriers, bounded carriers, bounded spaces, and Dirac laws.

Main statements

• TauCeti.wassersteinEDist_le and TauCeti.le_wassersteinEDist — the two halves of the universal property of the infimum, with TauCeti.wassersteinEDist_map_le providing the graph-plan pushforward bound, TauCeti.wassersteinEDist_lt_iff its order-theoretic restatement, and TauCeti.wassersteinEDist_eq_top_iff the characterization of an infinite value;
• TauCeti.wassersteinEDist_add_smul_dirac_le — the coupling estimate for moving part of a measure to a single point;
• TauCeti.wassersteinEDist_top — the p = ∞ characterization by coupling-wise essential suprema;
• TauCeti.eq_of_pairwise_edist_ge_of_wassersteinEDist_top_lt — on a uniformly separated space, measures at W_∞ distance below the separation scale agree;
• TauCeti.wassersteinEDist_self, TauCeti.wassersteinEDist_comm and TauCeti.wassersteinEDist_triangle — the three axioms of an extended pseudodistance;
• TauCeti.wassersteinEDist_le_add_edist_add_of_wassersteinEDist_dirac_le — measures within W_p-distance a, b of Diracs at x₀, x₁ are within a + d(x₀, x₁) + b of each other;
• TauCeti.wassersteinEDist_mono_exponent — monotonicity in p when the first marginal is a probability measure;
• TauCeti.wassersteinEDist_dirac_left, TauCeti.wassersteinEDist_dirac_right and TauCeti.wassersteinEDist_dirac_dirac — the unique-coupling identity W_p (δ_x, ν) = ‖edist x ·‖_{L^p (ν)}, its mirror image, and the two-Dirac value edist x y;
• TauCeti.wassersteinEDist_dirac_left_le_add and TauCeti.wassersteinEDist_dirac_left_ne_top — bounds for changing the basepoint, inside a fixed finite-distance component;
• TauCeti.memLp_edist_iff_wassersteinEDist_dirac_ne_top and TauCeti.memLp_edist_iff_of_edist_ne_top — the MemLp form of the Dirac identity and basepoint independence, with TauCeti.hasFiniteMoment_iff_memLp_edist and TauCeti.hasFiniteMoment_iff_wassersteinEDist_dirac_ne_top testing the finite-moment predicate itself at a prescribed basepoint of a pseudometric ground space;
• TauCeti.hasFiniteMoment_iff_wassersteinEDist_ne_top_of_hasFiniteMoment — the same test against a general finite-moment anchor, read off from TauCeti.memLp_edist_iff_hasFiniteMoment_of_isCoupling, which compares displacement and moment along a single coupling, and with TauCeti.hasFiniteMoment_iff_forall_hasFiniteMoment_iff_wassersteinEDist_ne_top recording that the finite-moment hypothesis on the anchor cannot be dropped;
• TauCeti.hasFiniteMoment_of_sum_mul_wassersteinEDist_rpow_ne_top — a law of finite weighted Wasserstein cost against finitely many laws, one of positive weight and finite moment, has finite moment;
• TauCeti.exists_notMem_dist_sq_add_dist_sq_le_of_wassersteinEDist_le — a probability measure W₂-close to two Dirac laws gives, off any null set, a point z with d(x₀, z)² + d(z, x₁)² ≤ 2 R²;
• TauCeti.HasFiniteMoment.smul_measure and TauCeti.HasFiniteMoment.add_measure — finite moments survive finite scalings and sums of finite measures, hence mixtures;
• TauCeti.HasFiniteMoment.integrable_of_lipschitzWith — a Lipschitz real function is integrable against a finite measure of finite first moment;
• TauCeti.HasFiniteMoment.memLp_id — on a seminormed additive group, a finite measure of finite p-moment has the identity in L^p, and TauCeti.memLp_of_hasFiniteMoment_map reads this off for a function from its law; TauCeti.integrable_norm_sub_sq_of_hasFiniteMoment deduces that the quadratic cost is integrable against a coupling of laws of finite second moment, and TauCeti.lintegral_edist_sq_eq_ofReal_integral rewrites its transport integral as a real one;
• TauCeti.wassersteinEDist_rpow_eq_transportCost and TauCeti.wassersteinEDist_eq_transportCost_rpow — for 0 < p < ∞, the exact bridge to Layer 1's transport cost of edist ^ p, with TauCeti.isOptimalCoupling_edist_rpow_iff identifying the minimizers, TauCeti.wassersteinEDist_one_eq_transportCost giving the case p = 1, and TauCeti.wassersteinEDist_rpow_le_lintegral the bound by the transport integral of a single coupling, and TauCeti.transportCost_edist_rpow_eq_top_of_not_hasFiniteMoment the infinite value against a target without finite moment;
• TauCeti.edist_rpow_le_mul_edist_rpow_add_mul_edist_rpow — the split upper bound K * (edist x₀ x ^ r + edist x₀ y ^ r) for the cost edist x y ^ r, with TauCeti.HasFiniteMoment.lintegral_const_mul_edist_rpow_ne_top its integrability under a finite p-moment;
• TauCeti.exists_isCoupling_eLpNorm_eq_wassersteinEDist — on a Polish space with a compatible extended pseudometric and for a finite nonzero exponent, between finite measures that admit a coupling, the infimum is attained;
• TauCeti.wassersteinEDist_eq_zero_iff — on such a space and for a finite nonzero exponent, W_p (μ, ν) = 0 exactly when μ = ν if the source measure is finite, with TauCeti.wassersteinEDist_top_eq_zero_iff giving the endpoint p = ∞ under the same finiteness hypothesis and TauCeti.eq_of_wassersteinEDist_eq_zero packaging the two into a single statement.

Implementation notes

The infimum is an iterated ⨅ over plans and over proofs of TauCeti.IsCoupling, matching TauCeti.transportCost: measures with no coupling at all — for instance two finite measures of different total mass — get the value ∞ with no case split, and TauCeti.wassersteinEDist_le is iInf₂_le.

The exponent is unrestricted in the definition. Only 1 ≤ p makes the triangle inequality true, and TauCeti.wassersteinEDist_exponent_zero records that the value collapses to 0 at p = 0 whenever the two measures are coupled at all. A theorem carries p ≠ 0 exactly when it needs it: the two-Dirac value, the transport-cost bridge, attainment and separation do, while the order-theoretic API, the vanishing on the diagonal, symmetry, the one-sided Dirac identities and TauCeti.wassersteinEDist_mono_exponent — monotonicity holds already from p = 0 — do not.

The measures are raw MeasureTheory.Measures, not bundled probability measures. Monotonicity in the exponent and the Dirac identities take the MeasureTheory.IsProbabilityMeasure instances they use. Attainment and separation apply to finite equal-mass measures by normalising and rescaling, while the order-theoretic API, symmetry and the vanishing on the diagonal hold for arbitrary measures.

The Dirac identities and basepoint-independence lemmas connect finite moments to finite-distance components. The metric structures on these components and on the finite-moment spaces P_p (X) are built in TauCeti.MeasureTheory.OptimalTransport.Wasserstein.Space.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 6, where W_p is defined by the same infimum and the triangle inequality is proved by the gluing lemma.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, AMS 2003, §7.1, Theorem 7.3 (the Wasserstein distances are distances).
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §5.1.

noncomputable def TauCeti.wassersteinEDist {X : Type u} [MeasurableSpace X] [EDist X] (p : ENNReal) (μ ν : MeasureTheory.Measure X) : ENNReal

The p-Wasserstein distance of μ and ν: the infimum, over the couplings π of μ and ν, of the L^p (π) seminorm of the ground extended distance fun z ↦ edist z.1 z.2.

It is ∞ when μ and ν have no coupling at all. For a jointly measurable ground distance the objective at p = ∞ is the π-essential supremum. Mathlib's MeasureTheory.eLpNorm makes the objective of a coupling π equal to ∞ when the ground distance is not almost everywhere strongly measurable for π. Without joint measurability that depends on π: when points are measurable, every function is almost everywhere constant for a Dirac coupling, and for p ≠ 0 its objective is the distance between the two points (TauCeti.wassersteinEDist_dirac_dirac, which assumes no measurability of the distance).

theorem TauCeti.wassersteinEDist_top {X : Type u} [MeasurableSpace X] [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (μ ν : MeasureTheory.Measure X) : wassersteinEDist ⊤ μ ν = ⨅ (π : MeasureTheory.Measure (X × X)), ⨅ (_ : IsCoupling π μ ν), MeasureTheory.eLpNormEssSup (fun (z : X × X) => edist z.1 z.2) π

At exponent ∞, the Wasserstein distance is the infimum of the coupling-wise essential suprema of a jointly measurable ground distance.

theorem TauCeti.wassersteinEDist_le {X : Type u} [MeasurableSpace X] [EDist X] {μ ν : MeasureTheory.Measure X} {π : MeasureTheory.Measure (X × X)} (hπ : IsCoupling π μ ν) (p : ENNReal) : wassersteinEDist p μ ν ≤ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π

Every coupling bounds the Wasserstein distance from above.

theorem TauCeti.wassersteinEDist_map_le {X : Type u} [MeasurableSpace X] [EDist X] {μ : MeasureTheory.Measure X} {T : X → X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hT : AEMeasurable T μ) (p : ENNReal) : wassersteinEDist p μ (MeasureTheory.Measure.map T μ) ≤ MeasureTheory.eLpNorm (fun (x : X) => edist x (T x)) p μ

The displacement bound. The Wasserstein distance from a law to its pushforward along a map is at most the L^p seminorm of the displacement x ↦ edist x (T x): the graph plan of T couples the two measures, and its objective is exactly that seminorm.

theorem TauCeti.le_wassersteinEDist {X : Type u} [MeasurableSpace X] {p a : ENNReal} [EDist X] {μ ν : MeasureTheory.Measure X} (h : ∀ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν → a ≤ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π) : a ≤ wassersteinEDist p μ ν

A bound valid on every coupling bounds the Wasserstein distance from below.

theorem TauCeti.wassersteinEDist_lt_iff {X : Type u} [MeasurableSpace X] {p a : ENNReal} [EDist X] {μ ν : MeasureTheory.Measure X} : wassersteinEDist p μ ν < a ↔ ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν ∧ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π < a

The Wasserstein distance is below a threshold exactly when some coupling is.

theorem TauCeti.eq_of_pairwise_edist_ge_of_wassersteinEDist_top_lt {Y : Type u_1} [MeasurableSpace Y] [EDist Y] {μ ν : MeasureTheory.Measure Y} {r : ENNReal} (hsep : Pairwise fun (x y : Y) => r ≤ edist x y) (h : wassersteinEDist ⊤ μ ν < r) : μ = ν

On a space whose distinct points are at least r apart, two measures at W_∞ distance strictly less than r agree. A coupling below the strict bound cannot move mass between distinct points. This also applies when the distance is infinite.

@[simp]

theorem TauCeti.wassersteinEDist_eq_top_iff {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {μ ν : MeasureTheory.Measure X} : wassersteinEDist p μ ν = ⊤ ↔ ∀ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν → MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π = ⊤

The Wasserstein distance is infinite exactly when every coupling has an infinite objective. Measures with no coupling at all satisfy the right-hand side vacuously.

theorem TauCeti.wassersteinEDist_eq_top_of_not_exists_isCoupling {X : Type u} [MeasurableSpace X] [EDist X] {μ ν : MeasureTheory.Measure X} (h : ¬∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν) (p : ENNReal) : wassersteinEDist p μ ν = ⊤

Measures with no coupling — by TauCeti.exists_isCoupling_iff, a finite measure and a measure of a different total mass — are at Wasserstein distance ∞.

theorem TauCeti.exists_isCoupling_of_wassersteinEDist_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {μ ν : MeasureTheory.Measure X} (h : wassersteinEDist p μ ν ≠ ⊤) : ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν

A finite Wasserstein distance is witnessed by a coupling. The converse fails: a coupling whose ground distance is not p-integrable leaves the value ∞.

theorem TauCeti.wassersteinEDist_exponent_zero {X : Type u} [MeasurableSpace X] [EDist X] {μ ν : MeasureTheory.Measure X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (h : ∃ (π : MeasureTheory.Measure (X × X)), IsCoupling π μ ν) : wassersteinEDist 0 μ ν = 0

At the exponent 0 the objective of a jointly measurable ground distance is identically 0, so the Wasserstein distance of any two coupled measures vanishes. Thus distance-specific results below exclude p = 0, although monotonicity in the exponent remains valid when its lower exponent is 0.

theorem TauCeti.wassersteinEDist_smul {X : Type u} [MeasurableSpace X] {p a : ENNReal} [EDist X] {μ ν : MeasureTheory.Measure X} (hc₀ : a ≠ 0) (hc_top : a ≠ ⊤) : wassersteinEDist p (a • μ) (a • ν) = a ^ (1 / p).toReal * wassersteinEDist p μ ν

Scaling both measures by the same nonzero finite factor scales their Wasserstein distance by the corresponding L^p factor. At p = ∞ this factor is one.

theorem TauCeti.wassersteinEDist_add_smul_dirac_le {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (p : ENNReal) (σ τ : MeasureTheory.Measure X) (x₀ : X) : wassersteinEDist p (σ + τ) (σ + τ Set.univ • MeasureTheory.Measure.dirac x₀) ≤ MeasureTheory.eLpNorm (fun (x : X) => edist x x₀) p τ

Moving a piece of mass to a single point. Replacing the part τ of the measure σ + τ by the Dirac mass at x₀ carrying the same total mass costs at most the L^p (τ) seminorm of the distance to x₀: the plan that leaves σ where it is and sends every point of τ to x₀ is a coupling of the two measures, and its objective is exactly that seminorm.

@[simp]

theorem TauCeti.wassersteinEDist_self {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [WeakPseudoEMetricSpace X] [MeasurableEq X] (p : ENNReal) (μ : MeasureTheory.Measure X) : wassersteinEDist p μ μ = 0

The Wasserstein distance from a measure to itself vanishes: the diagonal coupling has zero displacement almost everywhere.

Some measurability is unavoidable here — for the trivial σ-algebra on an unbounded metric space every coupling has infinite objective at p = ∞ — but a measurable diagonal is enough, and it is an instance rather than a side condition, which is what makes this usable as a simp lemma.

theorem TauCeti.wassersteinEDist_self_of_measurable_edist {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (p : ENNReal) (μ : MeasureTheory.Measure X) : wassersteinEDist p μ μ = 0

Wasserstein distance from a measure to itself vanishes when the ground extended distance is measurable. Unlike TauCeti.wassersteinEDist_self, this form does not require a measurable diagonal, which need not exist on a non-separated pseudometric Borel space.

theorem TauCeti.wassersteinEDist_comm {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (p : ENNReal) (μ ν : MeasureTheory.Measure X) : wassersteinEDist p μ ν = wassersteinEDist p ν μ

Symmetry. Exchanging the two measures does not change their Wasserstein distance.

theorem TauCeti.wassersteinEDist_mono_exponent {X : Type u} [MeasurableSpace X] {p q : ENNReal} [EDist X] (hpq : p ≤ q) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] : wassersteinEDist p μ ν ≤ wassersteinEDist q μ ν

Monotonicity in the exponent. If the first marginal is a probability measure, then the Wasserstein distance is monotone in p.

def TauCeti.HasFiniteMoment {X : Type u} [MeasurableSpace X] [EDist X] (p : ENNReal) (ν : MeasureTheory.Measure X) : Prop

A measure has finite p-moment if its extended distance from some basepoint belongs to L^p. On an extended pseudometric space, this condition refers to one finite-distance component; see TauCeti.memLp_edist_iff_of_edist_ne_top for independence within that component.

theorem TauCeti.hasFiniteMoment_def {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {ν : MeasureTheory.Measure X} : HasFiniteMoment p ν ↔ ∃ (x : X), MeasureTheory.MemLp (fun (y : X) => edist x y) p ν

A measure has finite p-moment exactly when its distance from some basepoint belongs to L^p.

theorem TauCeti.HasFiniteMoment.smul_measure {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {ν : MeasureTheory.Measure X} (h : HasFiniteMoment p ν) {c : ENNReal} (hc : c ≠ ⊤) : HasFiniteMoment p (c • ν)

Scaling a measure by a finite constant preserves finite p-moments.

@[simp]

theorem TauCeti.wassersteinEDist_dirac_left {X : Type u} [MeasurableSpace X] [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (p : ENNReal) (x : X) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist p (MeasureTheory.Measure.dirac x) ν = MeasureTheory.eLpNorm (fun (y : X) => edist x y) p ν

The unique-coupling identity. A Dirac source has exactly one coupling with each probability target, so the Wasserstein distance from δ x is the L^p (ν) seminorm of the ground distance to x. This is the identity that later identifies the finite-moment space P_p (X) with the finite-distance component of a Dirac law.

theorem TauCeti.memLp_edist_iff_wassersteinEDist_dirac_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (x : X) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.MemLp (fun (y : X) => edist x y) p ν ↔ wassersteinEDist p (MeasureTheory.Measure.dirac x) ν ≠ ⊤

The finite-moment condition about a specified basepoint is exactly finite Wasserstein distance from its Dirac measure.

theorem TauCeti.hasFiniteMoment_iff_exists_wassersteinEDist_dirac_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] : HasFiniteMoment p ν ↔ ∃ (x : X), wassersteinEDist p (MeasureTheory.Measure.dirac x) ν ≠ ⊤

The existential finite-moment predicate is equivalently finite Wasserstein distance from some Dirac measure.

@[simp]

theorem TauCeti.wassersteinEDist_dirac_dirac {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] [MeasurableSingletonClass X] (hp : p ≠ 0) (x y : X) : wassersteinEDist p (MeasureTheory.Measure.dirac x) (MeasureTheory.Measure.dirac y) = edist x y

The two-Dirac value. The only coupling of δ x with δ y is δ (x, y), so the Wasserstein distance of two Dirac measures is the ground distance of their atoms, for every nonzero exponent. This is the acceptance check W_p (δ_x, δ_y) = d (x, y).

Uniqueness of the coupling pins the infimum down without any measurability of the ground distance, which is also what makes this a usable simp lemma: the one-sided Dirac identities that would otherwise normalise its left-hand side all ask for a jointly measurable ground distance, so they do not fire here.

@[simp]

theorem TauCeti.wassersteinEDist_dirac_right {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (p : ENNReal) (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (y : X) : wassersteinEDist p μ (MeasureTheory.Measure.dirac y) = MeasureTheory.eLpNorm (fun (x : X) => edist x y) p μ

The mirror image of TauCeti.wassersteinEDist_dirac_left: the Wasserstein distance to a Dirac target is the L^p (μ) seminorm of the ground distance to the atom.

theorem TauCeti.wassersteinEDist_dirac_left_le_add {X : Type u} [MeasurableSpace X] {p : ENNReal} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) (x₀ x₁ : X) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist p (MeasureTheory.Measure.dirac x₁) ν ≤ edist x₁ x₀ + wassersteinEDist p (MeasureTheory.Measure.dirac x₀) ν

Moving the basepoint of the Dirac source costs at most the ground distance between the basepoints. See TauCeti.memLp_edist_iff_of_edist_ne_top for basepoint independence of the finite-moment condition.

theorem TauCeti.wassersteinEDist_triangle_dirac {X : Type u} [MeasurableSpace X] {p : ENNReal} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (y : X) : wassersteinEDist p μ (MeasureTheory.Measure.dirac y) ≤ wassersteinEDist p μ ν + wassersteinEDist p ν (MeasureTheory.Measure.dirac y)

The triangle inequality through a Dirac law. For probability measures, the Wasserstein distance to a Dirac law is at most the distance to any intermediate probability measure plus the distance from it to the Dirac law. A Dirac law has a single coupling with each probability measure, so no gluing, and hence no standard Borel hypothesis, is needed; compare TauCeti.wassersteinEDist_triangle.

theorem TauCeti.memLp_edist_iff_of_edist_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {x₀ x₁ : X} {ν : MeasureTheory.Measure X} (h₀ : MeasureTheory.AEStronglyMeasurable (fun (y : X) => edist x₀ y) ν) (h₁ : MeasureTheory.AEStronglyMeasurable (fun (y : X) => edist x₁ y) ν) (hx : edist x₁ x₀ ≠ ⊤) [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.MemLp (fun (y : X) => edist x₀ y) p ν ↔ MeasureTheory.MemLp (fun (y : X) => edist x₁ y) p ν

Finite p-moment about a basepoint is independent of the basepoint inside a fixed finite-distance component. On an extended pseudometric space the finite-distance hypothesis cannot be dropped: basepoints in different components can have unrelated moment conditions.

theorem TauCeti.wassersteinEDist_dirac_left_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) {x₀ x₁ : X} (hx : edist x₁ x₀ ≠ ⊤) (ν : MeasureTheory.Measure X) (h : wassersteinEDist p (MeasureTheory.Measure.dirac x₀) ν ≠ ⊤) : wassersteinEDist p (MeasureTheory.Measure.dirac x₁) ν ≠ ⊤

Finiteness of the Wasserstein distance from a Dirac source transfers to every basepoint at finite ground distance from the original basepoint.

theorem TauCeti.wassersteinEDist_triangle {X : Type u} [MeasurableSpace X] {p : ENNReal} [TopologicalSpace X] [WeakPseudoEMetricSpace X] [StandardBorelSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure ν] (ρ : MeasureTheory.Measure X) : wassersteinEDist p μ ρ ≤ wassersteinEDist p μ ν + wassersteinEDist p ν ρ

The triangle inequality. This holds for 1 ≤ p when the middle measure is finite and the measurable space is standard Borel.

theorem TauCeti.wassersteinEDist_le_add_edist_add_of_wassersteinEDist_dirac_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [TopologicalSpace X] [WeakPseudoEMetricSpace X] [StandardBorelSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp : 1 ≤ p) {x₀ x₁ : X} {μ₀ μ₁ : MeasureTheory.Measure X} {a b : ENNReal} (h₀ : wassersteinEDist p (MeasureTheory.Measure.dirac x₀) μ₀ ≤ a) (h₁ : wassersteinEDist p (MeasureTheory.Measure.dirac x₁) μ₁ ≤ b) : wassersteinEDist p μ₀ μ₁ ≤ a + edist x₀ x₁ + b

Two measures within W_p-distance a and b of Dirac masses at x₀ and x₁ are within W_p-distance a + edist x₀ x₁ + b of each other.

theorem TauCeti.hasFiniteMoment_dirac {X : Type u} [MeasurableSpace X] [PseudoEMetricSpace X] [OpensMeasurableSpace X] (p : ENNReal) (x : X) : HasFiniteMoment p (MeasureTheory.Measure.dirac x)

A Dirac law has finite p-moment for every exponent: its distance from its atom vanishes almost everywhere.

theorem TauCeti.HasFiniteMoment.memLp {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] {ν : MeasureTheory.Measure X} (h : HasFiniteMoment p ν) {x : X} (hd : MeasureTheory.AEStronglyMeasurable (fun (y : X) => edist x y) ν) [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.MemLp (fun (y : X) => edist x y) p ν

On an ordinary pseudometric space, a finite measure with finite p-moment at some basepoint has finite p-moment at every basepoint whose distance section is almost-everywhere strongly measurable.

theorem TauCeti.HasFiniteMoment.integrable_of_lipschitzWith {X : Type u} [MeasurableSpace X] [PseudoMetricSpace X] [OpensMeasurableSpace X] {ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure ν] (h : HasFiniteMoment 1 ν) {K : NNReal} {f : X → ℝ} (hf : LipschitzWith K f) : MeasureTheory.Integrable f ν

A Lipschitz real function is integrable against a finite measure with finite first moment: it grows at most linearly in the distance to a basepoint. These are the test functions of the Kantorovich–Rubinstein formula for W₁.

theorem TauCeti.hasFiniteMoment_of_ae_mem_of_isBounded {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] {ν : MeasureTheory.Measure X} {s : Set X} [MeasureTheory.IsFiniteMeasure ν] (x₀ : X) (hs : Bornology.IsBounded s) (hν : ∀ᵐ (y : X) ∂ν, y ∈ s) : HasFiniteMoment p ν

A finite measure carried by a bounded set has finite p-moment for every exponent: the ground distance to a basepoint is bounded on that set.

theorem TauCeti.hasFiniteMoment_of_ae_mem_finset {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] {ν : MeasureTheory.Measure X} {s : Finset X} [MeasureTheory.IsFiniteMeasure ν] (x₀ : X) (hs : ∀ᵐ (y : X) ∂ν, y ∈ s) : HasFiniteMoment p ν

A finite measure carried by a finite set has finite p-moment for every exponent: the ground distance to a basepoint is bounded on that finite set.

theorem TauCeti.hasFiniteMoment_of_boundedSpace {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] [BoundedSpace X] [Nonempty X] (ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure ν] : HasFiniteMoment p ν

On a nonempty bounded pseudometric space, for instance a nonempty compact one, every finite measure has finite p-moment for every exponent: the ground distance is bounded.

theorem TauCeti.hasFiniteMoment_iff_memLp_edist {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] {x : X} {ν : MeasureTheory.Measure X} (hd : MeasureTheory.AEStronglyMeasurable (fun (y : X) => edist x y) ν) [MeasureTheory.IsFiniteMeasure ν] : HasFiniteMoment p ν ↔ MeasureTheory.MemLp (fun (y : X) => edist x y) p ν

On an ordinary pseudometric space, the finite-moment condition can be tested at any prescribed basepoint whose distance section is almost-everywhere strongly measurable.

theorem TauCeti.hasFiniteMoment_iff_lintegral_edist_rpow_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] (hp0 : p ≠ 0) (hp : p ≠ ⊤) (x : X) (ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure ν] : HasFiniteMoment p ν ↔ ∫⁻ (y : X), edist x y ^ p.toReal ∂ν ≠ ⊤

For a finite nonzero exponent p, the finite-moment condition for a finite measure is equivalent to finiteness of its p-moment about any basepoint.

theorem TauCeti.HasFiniteMoment.lintegral_const_mul_edist_rpow_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] {ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure ν] (hν : HasFiniteMoment p ν) (hp0 : p ≠ 0) (hp : p ≠ ⊤) (x : X) {c : ENNReal} (hc : c ≠ ⊤) : ∫⁻ (y : X), c * edist x y ^ p.toReal ∂ν ≠ ⊤

For a finite nonzero exponent p, a finite measure with finite p-moment integrates every finite multiple of the p-th power of the distance to a basepoint to a finite value; this is the integrability half of the split upper bound for the cost edist ^ p.

theorem TauCeti.HasFiniteMoment.add_measure {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure ν] (hμ : HasFiniteMoment p μ) (hν : HasFiniteMoment p ν) : HasFiniteMoment p (μ + ν)

Adding a finite measure with finite p-moment preserves finite p-moment.

theorem TauCeti.hasFiniteMoment_iff_wassersteinEDist_dirac_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (x : X) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] : HasFiniteMoment p ν ↔ wassersteinEDist p (MeasureTheory.Measure.dirac x) ν ≠ ⊤

On an ordinary pseudometric space, the finite-moment condition is equivalent to finite Wasserstein distance from the Dirac law at any prescribed basepoint.

theorem TauCeti.memLp_edist_iff_hasFiniteMoment_of_isCoupling {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) {x₀ : X} {μ₀ ν : MeasureTheory.Measure X} {π : MeasureTheory.Measure (X × X)} [MeasureTheory.IsFiniteMeasure ν] (hπ : IsCoupling π μ₀ ν) (hx₀ : MeasureTheory.MemLp (fun (y : X) => edist x₀ y) p μ₀) : MeasureTheory.MemLp (fun (z : X × X) => edist z.1 z.2) p π ↔ HasFiniteMoment p ν

Displacement versus moment along a coupling. If the first marginal of π has finite p-moment at x₀, then the L^p (π) displacement is finite exactly when the second marginal has finite p-moment.

theorem TauCeti.hasFiniteMoment_iff_wassersteinEDist_ne_top_of_hasFiniteMoment {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) {μ₀ ν : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ₀] [MeasureTheory.IsProbabilityMeasure ν] (hμ₀ : HasFiniteMoment p μ₀) : HasFiniteMoment p ν ↔ wassersteinEDist p μ₀ ν ≠ ⊤

A probability measure has finite p-moment exactly when it lies at finite p-Wasserstein distance from a finite-moment anchor.

The hypothesis on the anchor is necessary, and TauCeti.hasFiniteMoment_iff_forall_hasFiniteMoment_iff_wassersteinEDist_ne_top records that guardrail: an infinite-moment probability law always belongs to its own finite-distance component, but it does not have finite moment.

theorem TauCeti.hasFiniteMoment_iff_forall_hasFiniteMoment_iff_wassersteinEDist_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (μ₀ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ₀] : HasFiniteMoment p μ₀ ↔ ∀ (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν], HasFiniteMoment p ν ↔ wassersteinEDist p μ₀ ν ≠ ⊤

Finite moment of the anchor is exactly the condition under which its finite-distance component is the finite-moment space: the criterion above holds for every probability law if and only if the anchor itself has finite p-moment.

theorem TauCeti.hasFiniteMoment_of_sum_mul_wassersteinEDist_rpow_ne_top {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) {ι : Type u_1} {s : Finset ι} {w : ι → ENNReal} {μ : ι → MeasureTheory.Measure X} {ν : MeasureTheory.Measure X} {i : ι} (hi : i ∈ s) (hwi : w i ≠ 0) [MeasureTheory.IsFiniteMeasure (μ i)] (hμ : HasFiniteMoment p (μ i)) {q : ℝ} (hq : 0 < q) (h : ∑ j ∈ s, w j * wassersteinEDist p ν (μ j) ^ q ≠ ⊤) : HasFiniteMoment p ν

A measure of finite weighted Wasserstein cost ∑ j ∈ s, w j * W_p(ν, μ j) ^ q has finite p-moment, provided some law μ i with i ∈ s of positive weight has finite p-moment and 0 < q: the corresponding summand bounds W_p(ν, μ i).

theorem TauCeti.exists_notMem_dist_sq_add_dist_sq_le_of_wassersteinEDist_le {X : Type u} [MeasurableSpace X] [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] {s : Set X} (hs : ν s = 0) {x₀ x₁ : X} {R : ℝ} (hR : 0 ≤ R) (h₀ : wassersteinEDist 2 (MeasureTheory.Measure.dirac x₀) ν ≤ ENNReal.ofReal R) (h₁ : wassersteinEDist 2 (MeasureTheory.Measure.dirac x₁) ν ≤ ENNReal.ofReal R) : ∃ z ∉ s, dist x₀ z ^ 2 + dist z x₁ ^ 2 ≤ 2 * R ^ 2

A point near two Dirac laws. If a probability measure ν is within W₂-distance R of both δ_{x₀} and δ_{x₁}, then outside any ν-null set s there is a point z with d(x₀, z)² + d(z, x₁)² ≤ 2 R²: the two second moments of ν add up to at most 2 R², and some point off s lies below their mean.

theorem TauCeti.lintegral_edist_sq_eq_ofReal_integral {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] {π : MeasureTheory.Measure (E × E)} (hπ : MeasureTheory.Integrable (fun (z : E × E) => ‖z.1 - z.2‖ ^ 2) π) : ∫⁻ (z : E × E), edist z.1 z.2 ^ 2 ∂π = ENNReal.ofReal (∫ (z : E × E), ‖z.1 - z.2‖ ^ 2 ∂π)

For an integrable quadratic cost, the transport integral of the squared extended distance is the real transport integral of the squared norm of the displacement.

theorem TauCeti.HasFiniteMoment.memLp_id {p : ENNReal} {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ν] (h : HasFiniteMoment p ν) : MeasureTheory.MemLp id p ν

On a seminormed additive group, a finite measure with finite p-moment has the identity in L^p: its distance from the basepoint 0 is the norm.

theorem TauCeti.memLp_of_hasFiniteMoment_map {q : ENNReal} {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {α : Type u_2} [MeasurableSpace α] {π : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure π] {f : α → E} (hf : AEMeasurable f π) (h : HasFiniteMoment q (MeasureTheory.Measure.map f π)) : MeasureTheory.MemLp f q π

A function whose law under a finite measure has finite q-th moment lies in Lq.

theorem TauCeti.integrable_norm_sub_sq_of_hasFiniteMoment {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {π : MeasureTheory.Measure (E × E)} [MeasureTheory.IsFiniteMeasure π] (h₁ : HasFiniteMoment 2 π.fst) (h₂ : HasFiniteMoment 2 π.snd) : MeasureTheory.Integrable (fun (z : E × E) => ‖z.1 - z.2‖ ^ 2) π

The quadratic cost ‖x - y‖² is integrable against a finite measure on E × E whose two marginals have finite second moment.

theorem TauCeti.memLp_sub_of_hasFiniteMoment {p : ENNReal} {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {π : MeasureTheory.Measure (E × E)} [MeasureTheory.IsFiniteMeasure π] (h₁ : HasFiniteMoment p π.fst) (h₂ : HasFiniteMoment p π.snd) : MeasureTheory.MemLp (fun (z : E × E) => z.2 - z.1) p π

The displacement (x, y) ↦ y - x belongs to L^p of a finite measure on E × E whose two marginals have finite p-moment.

theorem TauCeti.wassersteinEDist_rpow_le_lintegral {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) {μ ν : MeasureTheory.Measure X} {π : MeasureTheory.Measure (X × X)} (hπ : IsCoupling π μ ν) : wassersteinEDist p μ ν ^ p.toReal ≤ ∫⁻ (z : X × X), edist z.1 z.2 ^ p.toReal ∂π

For a finite nonzero exponent, every coupling bounds the p-th power of the Wasserstein distance by its transport integral of edist ^ p.

theorem TauCeti.wassersteinEDist_rpow_eq_transportCost {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) (μ ν : MeasureTheory.Measure X) : wassersteinEDist p μ ν ^ p.toReal = transportCost (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) μ ν

The bridge to the primal Kantorovich problem. For a finite nonzero exponent the p-th power of the Wasserstein distance is the transport cost of the cost edist ^ p, so the two infima — one of L^p seminorms, one of integrals — are the same optimisation problem.

theorem TauCeti.isOptimalCoupling_edist_rpow_iff {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {π : MeasureTheory.Measure (X × X)} {μ ν : MeasureTheory.Measure X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) : IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) π μ ν ↔ IsCoupling π μ ν ∧ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π = wassersteinEDist p μ ν

A coupling minimizes the p-power transport cost exactly when its L^p displacement realizes the Wasserstein infimum. This connects Wasserstein minimizers to the existing optimal-coupling API.

theorem TauCeti.IsOptimalCoupling.lintegral_edist_rpow_eq {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) {μ ν : MeasureTheory.Measure X} {π : MeasureTheory.Measure (X × X)} (hπ : IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) π μ ν) : ∫⁻ (z : X × X), edist z.1 z.2 ^ p.toReal ∂π = wassersteinEDist p μ ν ^ p.toReal

For a finite nonzero exponent, the transport integral of edist ^ p against an optimal coupling for that cost is the p-th power of the Wasserstein distance.

theorem TauCeti.IsOptimalCoupling.memLp_edist {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) {μ ν : MeasureTheory.Measure X} {π : MeasureTheory.Measure (X × X)} (hπ : IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) π μ ν) (hfin : wassersteinEDist p μ ν ≠ ⊤) : MeasureTheory.MemLp (fun (z : X × X) => edist z.1 z.2) p π

At finite Wasserstein distance and for a finite nonzero exponent, the ground distance lies in L^p of an optimal coupling for the cost edist ^ p.

theorem TauCeti.wassersteinEDist_eq_transportCost_rpow {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) (μ ν : MeasureTheory.Measure X) : wassersteinEDist p μ ν = transportCost (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) μ ν ^ (1 / p.toReal)

The root form of TauCeti.wassersteinEDist_rpow_eq_transportCost: for a finite nonzero exponent the Wasserstein distance is the p-th root of the transport cost of edist ^ p.

theorem TauCeti.wassersteinEDist_one_eq_transportCost {X : Type u} [MeasurableSpace X] [EDist X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (μ ν : MeasureTheory.Measure X) : wassersteinEDist 1 μ ν = transportCost (fun (z : X × X) => edist z.1 z.2) μ ν

At the exponent 1 the Wasserstein distance is the transport cost of the ground distance itself: the Kantorovich–Rubinstein problem is the primal problem for the cost edist.

theorem TauCeti.IsOptimalCoupling.lintegral_enorm_sub_rpow_eq {p : ENNReal} {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {μ ν : MeasureTheory.Measure E} {π : MeasureTheory.Measure (E × E)} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (hπ : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) π μ ν) : ∫⁻ (z : E × E), ‖z.2 - z.1‖ₑ ^ p.toReal ∂π = wassersteinEDist p μ ν ^ p.toReal

For a finite nonzero exponent, the p-th moment of the displacement (x, y) ↦ y - x under an optimal coupling for the cost ‖x - y‖ ^ p is the p-th power of the Wasserstein distance.

theorem TauCeti.IsOptimalCoupling.memLp_sub {p : ENNReal} {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {μ ν : MeasureTheory.Measure E} {π : MeasureTheory.Measure (E × E)} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (hπ : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) π μ ν) (hfin : wassersteinEDist p μ ν ≠ ⊤) : MeasureTheory.MemLp (fun (z : E × E) => z.2 - z.1) p π

At finite Wasserstein distance and for a finite nonzero exponent, the displacement (x, y) ↦ y - x lies in L^p of an optimal coupling for the cost ‖x - y‖ ^ p.

theorem TauCeti.transportCost_edist_rpow_eq_top_of_not_hasFiniteMoment {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : HasFiniteMoment p μ) (hν : ¬HasFiniteMoment p ν) : transportCost (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) μ ν = ⊤

Without a finite p-moment on the target, the transport cost of edist ^ p from a law of finite p-moment is infinite, for 0 < p < ∞.

theorem TauCeti.exists_isCoupling_eLpNorm_eq_wassersteinEDist {p : ENNReal} {X : Type u} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (hp0 : p ≠ 0) (hp : p ≠ ⊤) (μ ν : 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) p π = wassersteinEDist p μ ν

Attainment. On a Polish space with a compatible extended pseudometric and for a finite nonzero exponent, the infimum between two finite measures that admit a coupling is a minimum. The chosen extended pseudometric need not be complete.

theorem TauCeti.wassersteinEDist_eq_zero_iff {p : ENNReal} {X : Type u} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (hp0 : p ≠ 0) (hp : p ≠ ⊤) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : wassersteinEDist p μ ν = 0 ↔ μ = ν

Separation of measures. On a Polish space with a compatible extended pseudometric and for a finite nonzero exponent, the Wasserstein distance between finite measures vanishes exactly when they are equal. Polishness ensures that zero ground distance separates points.

theorem TauCeti.wassersteinEDist_top_eq_zero_iff {X : Type u} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : wassersteinEDist ⊤ μ ν = 0 ↔ μ = ν

Separation at the infinite exponent. On a Polish space with a compatible extended pseudometric, the infinite-exponent Wasserstein distance between finite measures vanishes exactly when they are equal. Only the first measure is assumed finite: finite distance supplies a coupling, so the second has the same finite mass.

theorem TauCeti.eq_of_wassersteinEDist_eq_zero {p : ENNReal} {X : Type u} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (hp : p ≠ 0) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (h : wassersteinEDist p μ ν = 0) : μ = ν

Separation of measures, uniformly in the exponent. On a Polish space with a compatible extended pseudometric, two finite measures at zero p-Wasserstein distance are equal, for every nonzero exponent. This packages TauCeti.wassersteinEDist_eq_zero_iff together with its endpoint TauCeti.wassersteinEDist_top_eq_zero_iff, so that consumers need not repeat the case split on p = ∞.