Wasserstein-1 distance via Kantorovich–Rubinstein duality (cost-generic)

The optimal-transport core, all generic over the underlying (pseudo)metric space — no Vlasov / phase-space dependency. Contents: the cost-parameterized functional wassersteinCost, the W₁ distance wasserstein1 (the c = dist case), the truncated-metric variant wassersteinBar (Wbar), and their property lemmas (symmetry, triangle, non-expansion under 1-Lipschitz pushforward, KR-dual lower bound, finiteness under finite first moments).

noncomputable def Vlasov.wassersteinCost {α : Type u_1} [MeasurableSpace α] (c : α → α → ℝ) (μ ν : MeasureTheory.Measure α) : ENNReal

Cost-parameterized Wasserstein-1 functional. KR-dual sup over functions whose oscillation is controlled by a cost c. Using the explicit oscillation bound |f x − f y| ≤ c x y (rather than LipschitzWith 1 f w.r.t. an ambient metric) decouples the definition from the PseudoMetricSpace instance, so a cost like min (dist x y) 1 (the truncated-metric "Wbar" cost) instantiates with no new instance. wasserstein1 is the c = dist case.

Equations

• Vlasov.wassersteinCost c μ ν = ⨆ (f : α → ℝ), ⨆ (_ : ∀ (x y : α), |f x - f y| ≤ c x y), ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), f x ∂ν)

theorem Vlasov.lipschitzWith_one_iff_oscillation {α : Type u_1} [PseudoMetricSpace α] (f : α → ℝ) : LipschitzWith 1 f ↔ ∀ (x y : α), |f x - f y| ≤ dist x y

The oscillation test class ∀ x y, |f x − f y| ≤ dist x y coincides with LipschitzWith 1 f for real-valued f on a pseudometric space. Bridge between wassersteinCost dist (the cost-parameterized form) and the LipschitzWith- phrased property lemmas.

noncomputable def Vlasov.wasserstein1 {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) : ENNReal

The Kantorovich–Rubinstein dual Wasserstein-1 distance: the c = dist case of wassersteinCost.

Equations

• Vlasov.wasserstein1 μ ν = Vlasov.wassersteinCost (fun (x y : α) => dist x y) μ ν

theorem Vlasov.wasserstein1_eq_iSup_lipschitz {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) : wasserstein1 μ ν = ⨆ (f : α → ℝ), ⨆ (_ : LipschitzWith 1 f), ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), f x ∂ν)

wasserstein1 equals the LipschitzWith 1-phrased sup. The property lemmas below rw through this; consumers reference wasserstein1 only through these property lemmas.

theorem Vlasov.wasserstein1_lt_top_of_finite_moment {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.Integrable (fun (y : E) => ‖y‖) μ) (hν : MeasureTheory.Integrable (fun (y : E) => ‖y‖) ν) : wasserstein1 μ ν < ⊤

For probability measures μ, ν on a normed space E with finite first moments (i.e. Integrable (fun y => ‖y‖) μ and same for ν), the Wasserstein-1 distance is finite: wasserstein1 μ ν < ⊤.

Proof sketch: For any 1-Lipschitz φ : E → ℝ, set ψ y := φ y - φ 0. Then |ψ(y)| ≤ ‖y‖ by 1-Lipschitz-ness, and ∫φdμ − ∫φdν = ∫ψdμ − ∫ψdν (the constants φ(0)·μ(univ) = φ(0)·ν(univ) cancel since both are probability measures). So ∫φdμ − ∫φdν ≤ ∫|ψ|dμ + ∫|ψ|dν ≤ ∫‖y‖dμ + ∫‖y‖dν =: M, finite. Taking sup over 1-Lip φ: wasserstein1 μ ν ≤ ENNReal.ofReal M < ⊤.

theorem Vlasov.wasserstein1_ne_top_of_finite_moment {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.Integrable (fun (y : E) => ‖y‖) μ) (hν : MeasureTheory.Integrable (fun (y : E) => ‖y‖) ν) : wasserstein1 μ ν ≠ ⊤

Convenience corollary: under the same hypotheses, wasserstein1 μ ν ≠ ⊤.

Basic algebra of wasserstein1

The KR-dual sup-formula makes wasserstein1 a pseudometric on Measure α (we only get a pseudo-metric, not a metric, because wasserstein1 μ ν = 0 does not characterise μ = ν in this generality). The three lemmas below are self-distance / symmetry / triangle, all derived directly from the sup-formula. Together they make wasserstein1 usable as the codomain of a sup-W₁ pseudo- distance on time-indexed measure curves (see supW1On in LeanPool/Vlasov/OT/CharacteristicFlow.lean).

theorem Vlasov.wassersteinCost_self {α : Type u_1} [MeasurableSpace α] (c : α → α → ℝ) (μ : MeasureTheory.Measure α) : wassersteinCost c μ μ = 0

wassersteinCost c μ μ = 0 (cost-generic; no hypothesis on c). Self-distance is zero; wasserstein1_self is the c = dist corollary.

theorem Vlasov.wasserstein1_self {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ : MeasureTheory.Measure α) : wasserstein1 μ μ = 0

theorem Vlasov.wassersteinCost_comm {α : Type u_1} [MeasurableSpace α] (c : α → α → ℝ) (μ ν : MeasureTheory.Measure α) : wassersteinCost c μ ν = wassersteinCost c ν μ

Symmetry: wassersteinCost c μ ν = wassersteinCost c ν μ. The oscillation test class |f x − f y| ≤ c x y is closed under f ↦ −f, so no symmetry assumption on c is needed.

theorem Vlasov.wasserstein1_comm {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) : wasserstein1 μ ν = wasserstein1 ν μ

theorem Vlasov.wassersteinCost_triangle {α : Type u_1} [MeasurableSpace α] (c : α → α → ℝ) (μ ν τ : MeasureTheory.Measure α) : wassersteinCost c μ τ ≤ wassersteinCost c μ ν + wassersteinCost c ν τ

Triangle inequality: wassersteinCost c μ τ ≤ wassersteinCost c μ ν + wassersteinCost c ν τ. No triangle assumption on c — the inequality is the test-function integral decomposition (the same f is valid for all three costs wassersteinCost c · ·).

theorem Vlasov.wasserstein1_triangle {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν τ : MeasureTheory.Measure α) : wasserstein1 μ τ ≤ wasserstein1 μ ν + wasserstein1 ν τ

theorem Vlasov.wasserstein1_le_moments_sum {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.Integrable (fun (y : E) => ‖y‖) μ) (hν : MeasureTheory.Integrable (fun (y : E) => ‖y‖) ν) : wasserstein1 μ ν ≤ ENNReal.ofReal (∫ (y : E), ‖y‖ ∂μ + ∫ (y : E), ‖y‖ ∂ν)

Quantitative finite-moment bound for wasserstein1: the W₁ distance is bounded by the sum of the two measures' first moments.

This refines wasserstein1_lt_top_of_finite_moment (which only states ≠⊤) by providing the explicit upper bound ∫‖y‖dμ + ∫‖y‖dν. Used by the sup-W₁ pseudodistance on VlasovMeasureCurves to derive finiteness from the uniform first-moment bound.

theorem Vlasov.wassersteinCost_le_of_lipschitz_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [PseudoMetricSpace β] [OpensMeasurableSpace β] (c_α : α → α → ℝ) (c_β : β → β → ℝ) (hc_β_le : ∀ (x y : β), c_β x y ≤ dist x y) (T : α → β) (L : NNReal) (hT_cost : ∀ (x y : α), c_β (T x) (T y) ≤ ↑L * c_α x y) (hT_meas : Measurable T) (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinCost c_β (MeasureTheory.Measure.map T μ) (MeasureTheory.Measure.map T ν) ≤ ↑L * wassersteinCost c_α μ ν

Cost-generic non-expansion under Lipschitz pushforward.

If T : α → β is L-Lipschitz with respect to the costs (c_β (T x) (T y) ≤ L · c_α x y) and c_β is dominated by the metric on β (c_β x y ≤ dist x y, which makes every c_β-oscillation test function 1-Lipschitz, hence continuous and measurable — what integral_map needs), then pushforward by T is L-non-expansive in wassersteinCost: wassersteinCost c_β (T_# μ) (T_# ν) ≤ L · wassersteinCost c_α μ ν.

wasserstein1_le_of_lipschitz_map (c = dist, below) and the Wbar analog (c = fun x y => min (dist x y) 1) are instances.

theorem Vlasov.wasserstein1_le_of_lipschitz_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoMetricSpace α] [MeasurableSpace β] [PseudoMetricSpace β] [OpensMeasurableSpace β] (T : α → β) (L : NNReal) (hT : LipschitzWith L T) (hT_meas : Measurable T) (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wasserstein1 (MeasureTheory.Measure.map T μ) (MeasureTheory.Measure.map T ν) ≤ ↑L * wasserstein1 μ ν

W₁ non-expansion under Lipschitz pushforward — the c = dist instance of wassersteinCost_le_of_lipschitz_map.

theorem Vlasov.wassersteinCost_dual_lower_bound {α : Type u_1} [MeasurableSpace α] (c : α → α → ℝ) (μ ν : MeasureTheory.Measure α) (f : α → ℝ) (hf : ∀ (x y : α), |f x - f y| ≤ c x y) : ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), f x ∂ν) ≤ wassersteinCost c μ ν

KR-dual lower bound for wasserstein1.

For any 1-Lipschitz f : α → ℝ and any measures μ, ν on a pseudo-metric measurable space, the (positive part of the) integral difference is a lower bound on W₁(μ, ν): ENNReal.ofReal (∫ f dμ - ∫ f dν) ≤ wasserstein1 μ ν.

This is the "easy direction" of the Kantorovich-Rubinstein dual characterization — it is built into the definition wasserstein1 := ⨆ f hf, ENNReal.ofReal (∫ f dμ - ∫ f dν) and follows by le_iSup.

Chained with f → -f 1-Lipschitz, it gives the "W₁=0 → ∫f dμ = ∫f dν for 1-Lipschitz f" reduction used by the separation lemma wasserstein1_eq_zero_iff_measure_eq.

Cost-generic: stated below for wassersteinCost c with f of c-oscillation, no hypothesis on c; wasserstein1_dual_lower_bound is the c = dist corollary.

theorem Vlasov.wasserstein1_dual_lower_bound {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) (f : α → ℝ) (hf : LipschitzWith 1 f) : ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), f x ∂ν) ≤ wasserstein1 μ ν

wassersteinBar — the truncated (cutoff) Wasserstein-1 distance Wbar

Wbar := wassersteinCost (min(dist, 1)) (Dobrushin 1979 §5). The bounded cost makes the dual test class bounded 1-Lipschitz (oscillation ≤ 1); on probability measures this classically makes Wbar finite without moment hypotheses and lets it metrize narrow convergence — neither fact is needed, or proved, in this development. The property layer below instantiates verbatim from the cost-generic lemmas: min(dist, 1) is a continuous pseudometric dominated by dist, so every hypothesis is met.

noncomputable def Vlasov.wassersteinBar {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) : ENNReal

The truncated Wasserstein-1 distance Wbar (Dobrushin 1979 §5): the c = min(dist, 1) instance of wassersteinCost.

Equations

• Vlasov.wassersteinBar μ ν = Vlasov.wassersteinCost (fun (x y : α) => min (dist x y) 1) μ ν

theorem Vlasov.wassersteinBar_self {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ : MeasureTheory.Measure α) : wassersteinBar μ μ = 0

theorem Vlasov.wassersteinBar_comm {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) : wassersteinBar μ ν = wassersteinBar ν μ

theorem Vlasov.wassersteinBar_triangle {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν τ : MeasureTheory.Measure α) : wassersteinBar μ τ ≤ wassersteinBar μ ν + wassersteinBar ν τ

theorem Vlasov.wassersteinBar_dual_lower_bound {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (μ ν : MeasureTheory.Measure α) (f : α → ℝ) (hf : ∀ (x y : α), |f x - f y| ≤ min (dist x y) 1) : ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), f x ∂ν) ≤ wassersteinBar μ ν

theorem Vlasov.wassersteinBar_le_of_lipschitz_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoMetricSpace α] [MeasurableSpace β] [PseudoMetricSpace β] [OpensMeasurableSpace β] (T : α → β) (hT : LipschitzWith 1 T) (hT_meas : Measurable T) (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinBar (MeasureTheory.Measure.map T μ) (MeasureTheory.Measure.map T ν) ≤ wassersteinBar μ ν

Wbar non-expansion under 1-Lipschitz pushforward: Wbar(T_# μ, T_# ν) ≤ Wbar(μ, ν). The cost-Lipschitz hypothesis is min(dist(Tx,Ty),1) ≤ min(dist x y, 1) (from dist(Tx,Ty) ≤ dist x y).

theorem Vlasov.integral_boundedContinuous_eq_of_integral_lipschitz_eq {α : Type u_1} [MeasurableSpace α] [NormedAddCommGroup α] [BorelSpace α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (_h_1lip : ∀ (f : α → ℝ), LipschitzWith 1 f → MeasureTheory.Integrable f μ → MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂μ = ∫ (x : α), f x ∂ν) (f : BoundedContinuousFunction α ℝ) : ∫ (x : α), f x ∂μ = ∫ (x : α), f x ∂ν

Bounded-continuous integral equality from 1-Lipschitz integral equality.

For probability measures μ, ν on a normed AddCommGroup α with the Borel σ-algebra, both having finite first moments, if ∫ f dμ = ∫ f dν for every 1-Lipschitz function f : α → ℝ (with appropriate integrability), then the same equality holds for every bounded continuous function f : α →ᵇ ℝ.

Proof.

• Step A: upgrade the 1-Lipschitz hypothesis to arbitrary K-Lipschitz integrable functions by scaling into the 1-Lipschitz class (c⁻¹ • g with c = K + 1).
• Step B: closed sets F receive equal measure. Thickened indicators thickenedIndicator δ F are bounded Lipschitz, so their integrals against μ and ν agree (Step A); letting δ → 0 and using tendsto_lintegral_thickenedIndicator_of_isClosed gives μ F = ν F.
• Closed sets form a π-system generating the Borel σ-algebra, so μ = ν by ext_of_generate_finite; equality of all BC integrals is then immediate.

Further wasserstein1 properties

(separation, narrow-liminf LSC, ofReal-exp monotonicity). 

theorem Vlasov.wasserstein1_eq_zero_iff_measure_eq {α : Type u_1} [MeasurableSpace α] [NormedAddCommGroup α] [BorelSpace α] [HasOuterApproxClosed α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wasserstein1 μ ν = 0 ↔ μ = ν

Separation lemma for wasserstein1.

For probability measures μ, ν on a Polish normed space with finite first moments, W₁(μ, ν) = 0 iff μ = ν.

wasserstein1 enters the proof body only through its property lemmas:

• wasserstein1_self (backward direction).
• wasserstein1_dual_lower_bound (W₁=0 → 1-Lipschitz integral equality).

The substantive middle (1-Lipschitz equality → BC equality) is integral_boundedContinuous_eq_of_integral_lipschitz_eq (above); the final step (BC equality → μ = ν) routes through Mathlib's ext_of_forall_integral_eq_of_IsFiniteMeasure.

theorem Vlasov.wasserstein1_le_liminf_of_narrow {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure μ] (hμ_int : MeasureTheory.Integrable (fun (y : E) => ‖y‖) μ) (νs : ℕ → MeasureTheory.Measure E) (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] (hν_int : MeasureTheory.Integrable (fun (y : E) => ‖y‖) ν) (h_narrow : ∀ (g : BoundedContinuousFunction E ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : E), g x ∂νs n) Filter.atTop (nhds (∫ (x : E), g x ∂ν))) : wasserstein1 μ ν ≤ Filter.liminf (fun (n : ℕ) => wasserstein1 μ (νs n)) Filter.atTop

Static narrow lower-semicontinuity of wasserstein1 (Villani, Thm 6.9, in KR-dual form). If νs n → ν narrowly (tested against bounded continuous functions) and μ, ν have finite first moments, then W₁(μ, ν) ≤ liminf_n W₁(μ, νs n).

This is the static optimal-transport fact — pure lower semicontinuity of the metric under weak convergence, with no flow/superposition. Prokhorov supplies the narrow limit; this upgrades a W₁-Cauchy sequence to W₁-convergence. Distinct from the dynamic narrow continuity along a Vlasov flow, which genuinely needs DiPerna–Lions superposition; the static LSC does not.

Proof. For each 1-Lipschitz φ truncate to φ_k = clamp(φ, -k, k) (bounded and 1-Lipschitz). Narrow convergence gives ∫ φ_k d(νs n) → ∫ φ_k dν, and the dual lower bound gives ofReal(∫φ_k dμ − ∫φ_k d(νs n)) ≤ W₁(μ, νs n); passing to the liminf in n yields ofReal(∫φ_k dμ − ∫φ_k dν) ≤ liminf_n W₁(μ, νs n). Then k → ∞ by dominated convergence (|φ_k| ≤ |φ 0| + ‖·‖, integrable since μ, ν have finite first moment) recovers ofReal(∫φ dμ − ∫φ dν) ≤ liminf_n W₁. Taking the ⨆ over φ closes it. The narrow hypothesis is taken in bounded-continuous-test form (what ProbabilityMeasure.tendsto_iff_forall_integral_tendsto exposes), so the exists_wasserstein1_limit_of_cauchy caller feeds it directly from Prokhorov.

theorem Vlasov.wasserstein1_ofReal_exp_monotone (C : ℝ) (hC : 0 < C) (s t : ℝ) (hst : s ≤ t) : ENNReal.ofReal (Real.exp (C * s)) ≤ ENNReal.ofReal (Real.exp (C * t))

For C > 0 and 0 ≤ s ≤ t, we have ENNReal.ofReal (Real.exp (C * s)) ≤ ENNReal.ofReal (Real.exp (C * t)). This is the monotonicity of the exponential bound in time.

Equation (Dobrushin stability estimate) (tex: eq:dobrushin)