Coupling-based Wasserstein-1 distance #
OT infrastructure on pseudometric spaces:
- Couplings and the Monge-Kantorovich definition of
W_1. - The easy direction of Kantorovich-Rubinstein duality,
wasserstein1_dual μ ν ≤ wasserstein1Coupling μ ν. - The hard direction
wasserstein1Coupling μ ν ≤ wasserstein1_dual μ ν(via finite-range approximation + finite transportation LP duality), yielding the full KR equalitywasserstein1_eq_coupling.
The dobrushin proof uses the coupling-cost bound to control W₁ growth along characteristic flows.
See formalize/DESIGN.md (in the source repository) for the overall design choices.
Couplings #
A coupling of measures μ on α and ν on β is a measure π on the
product space whose marginals are exactly μ and ν.
We use the convention that Prod.fst is the α-marginal and Prod.snd is
the β-marginal.
Equations
- Vlasov.IsCoupling π μ ν = (MeasureTheory.Measure.map Prod.fst π = μ ∧ MeasureTheory.Measure.map Prod.snd π = ν)
Instances For
Coupling-based Wasserstein-1 distance #
The coupling-based Wasserstein-1 distance: infimum of ∫⁻ edist(x,y) dπ(x,y)
over all couplings π of (μ, ν). This is the Monge-Kantorovich definition,
to be compared with the dual definition wasserstein1 (in LeanPool/Vlasov/OT/Wasserstein.lean)
via Kantorovich-Rubinstein duality.
We use the Lebesgue lower integral ∫⁻ of edist (extended distance, valued
in ℝ≥0∞) rather than the Bochner integral ∫ of dist (valued in ℝ).
This is the standard OT convention: a coupling π whose cost is non-integrable
contributes ⊤ to the infimum (rather than the Bochner junk-value 0), so the
infimum correctly identifies the OT-optimal coupling. Returns ⊤ if no
coupling exists.
Equations
- Vlasov.wasserstein1Coupling μ ν = ⨅ (π : MeasureTheory.Measure (α × α)), ⨅ (_ : Vlasov.IsCoupling π μ ν), ∫⁻ (z : α × α), edist z.1 z.2 ∂π
Instances For
Kantorovich-Rubinstein: easy direction #
The dual-formula wasserstein1 is at most the coupling-formula
wasserstein1Coupling. The one-line argument in the OT literature:
for any 1-Lipschitz φ and any coupling π,
∫φ d(μ - ν) = ∫(φ x - φ y) dπ ≤ ∫ |φ x - φ y| dπ ≤ ∫ dist(x,y) dπ.
The reverse inequality is the hard direction wassersteinCostCoupling_le_dual.
KR easy direction. Under finite-moment assumptions on μ and ν, the
dual-formula wasserstein1 μ ν is bounded above by the coupling-formula
wasserstein1Coupling μ ν.
By iSup_le and le_iInf, it suffices to show that for every 1-Lipschitz φ
and every coupling π of (μ, ν):
ENNReal.ofReal (∫φ dμ − ∫φ dν) ≤ ∫⁻ edist z.1 z.2 ∂π. When the coupling cost
is ⊤ the bound is trivial; otherwise edist-integrability of π gives
dist-integrability, change of variables through the marginals rewrites
∫φ dμ - ∫φ dν = ∫(φ(z.1) - φ(z.2)) dπ, and |φ(z.1) - φ(z.2)| ≤ dist(z.1, z.2)
(1-Lipschitz) closes it (integrability via the finite first moments of μ, ν).
Hard Kantorovich–Rubinstein duality #
This section proves the hard direction wassersteinCostCoupling_le_dual
(coupling-inf ≤ dual-sup) and derives the KR equality from it together with the
easy direction above. Everything is stated cost-generically over a
continuous pseudometric cost c, so an alternative cutoff cost
c = min (dist ·) 1 instantiates the same statements verbatim.
Cost-generic coupling cost: the infimum over couplings π of (μ, ν) of
∫⁻ ofReal (c z.1 z.2) ∂π. At c = dist this is wasserstein1Coupling
(edist = ofReal ∘ dist); see wasserstein1Coupling_eq.
Equations
- Vlasov.wassersteinCostCoupling c μ ν = ⨅ (π : MeasureTheory.Measure (α × α)), ⨅ (_ : Vlasov.IsCoupling π μ ν), ∫⁻ (z : α × α), ENNReal.ofReal (c z.1 z.2) ∂π
Instances For
At c = dist, the cost-generic coupling cost reduces to wasserstein1Coupling
(since edist x y = ofReal (dist x y)).
Kantorovich–Rubinstein duality (hard direction) helpers #
The lemmas below decompose wassersteinCostCoupling_le_dual via discrete
approximation + limit. All are general optimal-transport facts (not
Vlasov-specific), stated cost-generically over a continuous pseudometric cost.
Symmetry of the coupling cost.
For a symmetric cost, wassersteinCostCoupling c μ ν = wassersteinCostCoupling c ν μ
(push a coupling forward under Prod.swap).
Gluing of couplings. Given a
coupling π₁ of (μ, ρ) and a coupling π₂ of (ρ, ν), disintegrating π₂ over
its ρ-marginal (condKernel) and re-binding along π₁'s ρ-marginal yields a
coupling π₃ of (μ, ν) whose cost is at most the sum of the two costs (ground-cost
triangle c x z ≤ c x y + c y z). The load-bearing facts are the two marginals
(map fst π₃ = μ via fst_compProd; map snd π₃ = ν via snd_compProd + the
bind/map/comap law).
Triangle inequality for the
coupling cost. Gluing of couplings through a common middle measure
(exists_coupling_glue), then the iInf arithmetic.
Graph-coupling bound. The
coupling cost between μ and a pushforward Measure.map T μ is at most the
integrated transport cost of T, witnessed by the graph coupling
(id, T)_# μ.
Finite-range step map construction.
Given a measurable pairwise-disjoint partition As : ℕ → Set α covering univ with
representatives as : ℕ → α and a fallback point x₀, the truncated step map
T x = as n when x ∈ As n for some n < N, T x = x₀ otherwise, is measurable
and has finite range contained in {as n | n < N} ∪ {x₀}.
Integrable nonneg → lintegral ofReal finite.
If f : α → ℝ is integrable with respect to μ and a.e. nonneg, then
∫⁻ x, ENNReal.ofReal (f x) ∂μ ≠ ∞.
Key tools: hasFiniteIntegral_iff_ofReal and Integrable.hasFiniteIntegral.
Tail cost control via absolute continuity.
If ∫⁻ x, ENNReal.ofReal (f x) ∂μ ≠ ∞ and μ ((S n)ᶜ) → 0 as n → ∞, then the tail
costs ∫⁻ x in (S n)ᶜ, ENNReal.ofReal (f x) ∂μ → 0.
Follows from MeasureTheory.tendsto_setLIntegral_zero (absolute continuity of the integral).
Kept-cells cost bound.
For a step map T with T x = as n on As n (for n < N), where we have a pointwise
bound ∀ n < N, ∀ x ∈ As n, c x (T x) ≤ δ (established from the cell diameter), the
lintegral of ENNReal.ofReal (c x (T x)) over the kept cells is at most ENNReal.ofReal δ
since μ univ = 1.
Tail mass of a measurable cover → 0.
For a finite measure and a measurable cover ⋃ n, As n = univ, the mass of the complement
of the partial unions ⋃ j < n, As j tends to 0 (continuity from above:
⋂ n (⋃ j<n As j)ᶜ = ∅).
Finite-range approximation. For a probability measure with finite first moment, the transport cost to a finite-range pushforward can be made arbitrarily small (partition into small-diameter cells + finite-moment tail control).
Finite transportation LP: compactness leaves #
Two standalone compactness facts underpinning the finite Kantorovich-duality kernel
finiteRange_transportation_dual:
exists_transport_min— the transport polytope{P ≥ 0 : rowsums = a, colsums = b}is compact and nonempty, so the primal cost⟨Cost, P⟩attains its minimum (extreme value theorem on a closed bounded polytope in the finite-dimensional spacem → n → ℝ).isClosed_transport_cone— the image coneΦ(orthant) = {(rowsums P, colsums P, ⟨Cost,P⟩ + s) : P ≥ 0, s ≥ 0}(marginals + relaxed cost coordinate, the slacksmaking the cost coordinate an inequality) is closed (Bolzano–Weierstrass), which is theProperConeobligation for the geometric Farkas separationProperCone.hyperplane_separation_point.
Both use the geometric ι → ℝ route (plain products, no EuclideanSpace inner-product
instances).
Primal attainment for the finite transportation LP. The feasible polytope
{P ≥ 0 : rowsums = a, colsums = b} is compact (closed + bounded in finite dimension) and
nonempty (it contains the product a ⊗ b), so the linear cost
⟨Cost, P⟩ = ∑ᵢⱼ Costᵢⱼ Pᵢⱼ attains its minimum on it.
Closedness of the transport image cone (the ProperCone obligation for geometric
Farkas). The image of the orthant {(P, s) : P ≥ 0, s ≥ 0} under the affine-marginal +
relaxed-cost map Φ(P, s) = (rowsums P, colsums P, ⟨Cost, P⟩ + s) is closed. Proof by
Bolzano–Weierstrass: a convergent sequence in the image has convergent marginals, hence the
matrices Pₖ are bounded (mass conservation), so a subsequence converges to a feasible limit
P* matching the limit marginals; the slack s* = (limit cost coord) − ⟨Cost, P*⟩ ≥ 0.
The transport image cone Φ(orthant) = {(rowsums P, colsums P, ⟨Cost,P⟩ + s) : P ≥ 0, s ≥ 0} packaged as a ProperCone over ℝ: a PointedCone (0, +, ℝ≥0-smul closure
— Φ is linear and the orthant a cone) that is closed (isClosed_transport_cone). This is
the ProperCone obligation for the geometric Farkas separation
ProperCone.hyperplane_separation_point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Per-ε Farkas separation. Given the optimal plan P (primal value V = ⟨Cost,P⟩),
for every ε > 0 there is a dual-feasible pair (u, v) whose value exceeds V − ε. Proof:
(a, b, V − ε) ∉ transportProperCone (no feasible plan beats V), so
ProperCone.hyperplane_separation_point yields a separating functional f; reading off
λ = f(0,0,1), Uᵢ = f(eᵢ,0,0), Wⱼ = f(0,eⱼ,0) gives Uᵢ + Wⱼ + λ·Costᵢⱼ ≥ 0 and
∑aᵢUᵢ + ∑bⱼWⱼ + λ(V−ε) < 0; λ > 0 is forced (else the optimal P contradicts the
strict inequality), and u = −U/λ, v = −W/λ are feasible with value > V − ε.
ε-approximate finite LP duality with optimal plan. Packages the primal optimum
P (exists_transport_min) with an ε-optimal dual pair (finiteTransport_dual_eps): for
every ε > 0, an optimal feasible plan P and a dual-feasible (u, v) with the primal
cost ⟨Cost, P⟩ within ε of the dual value. The downstream KR bridge then sends the ε to
the Kantorovich sup (no attainment needed — ε-optimal throughout).
Transportation dual potentials (ε-form).
For finite-range pushforwards Measure.map T μ, Measure.map S ν and every ε > 0, finite
transportation LP duality yields a measurable dual pair u, v with u a + v b ≤ c a b on the
supports range T, range S, whose value ∫u dμ' + ∫v dν' bounds the coupling infimum from
above up to ε. Proof: the finite LP gives (finiteTransport_dual_eps_plan) an optimal
plan P and a dual pair within ε; the matrix→measure bridge sends P to a coupling
realising coupling-inf ≤ ofReal⟨Cost,P⟩ and identifies ∫u dμ' = ∑ aᵢ uᵢ (integral against
a finitely-supported pushforward), and the dual potentials lift to measurable α → ℝ. The ε
is consumed at the Kantorovich sup downstream — no attainment needed. Metric-free: no
symmetry/triangle (those enter only in the c-transform cTransform_dual_witness).
c-transform: dual pair → single globally-admissible potential.
Given transportation dual potentials u, v with u a + v b ≤ c a b on the finite
supports and c a (pseudo)metric cost, the c-transform
g x = ⨆ a ∈ range T, (u a − c x a) is globally c-admissible
(|g x − g y| ≤ c x y, by triangle + symmetry) and dominates the dual value:
g a ≥ u a (the a' = a term, c a a = 0) and g b ≤ −v b
(from u a − c a b ≤ −v b), so ∫u dμ' + ∫v dν' ≤ ∫g dμ' − ∫g dν'. This is where
hc_triangle/hc_symm are load-bearing — it converts the Farkas dual pair into the
single 1-Lipschitz potential the Kantorovich dual sup ranges over.
Finite Kantorovich–Rubinstein
duality. For finitely-supported (finite-range pushforward) probability measures,
the coupling-infimum is at most the dual-supremum. Proof = finite transportation LP
duality (Farkas, finiteRange_transportation_dual) producing a dual pair, then the
c-transform (cTransform_dual_witness) converting it to a single globally-admissible
potential, which the dual sup dominates (le_iSup₂).
Single-map dual bound. The
dual cost between a pushforward Measure.map T μ and μ is at most the integrated
transport cost of T. Direct dual-side analogue of wassersteinCostCoupling_map_le:
for any c-admissible test f (oscillation ≤ c, hence continuous), the change of
variables ∫ f d(T_# μ) = ∫ f∘T dμ plus |f(Tx) − f x| ≤ c x (Tx) gives the bound;
the finite c-moment hμ_cm controls test-function integrability.
Dual-side stability under
pushforward. A c-admissible test function changes value by at most the
transport cost, so the dual sup over (T_# μ, S_# ν) exceeds that over (μ, ν)
by at most the two transport costs. Dual triangle (wassersteinCost_triangle)
through μ then ν, with each single-map leg bounded by
wassersteinCost_dual_singleMap_le.
Hard direction of Kantorovich–Rubinstein duality — the primal coupling-formula is at most the dual-formula.
For probability measures μ, ν with finite first moment on a Polish (here
second-countable Borel pseudometric, standard Borel) space and a continuous
pseudometric cost c: wassersteinCostCoupling c μ ν ≤ wassersteinCost c μ ν.
The reverse inequality is the easy direction
wasserstein1_le_wasserstein1Coupling; together they give the full KR equality
wasserstein1_eq_coupling.
This is an inf ≤ sup statement, so the infimum need not be attained — the bound
is reached ε-optimally. Stated cost-generically over a continuous pseudometric
c, so a cutoff cost c = min (dist ·) 1 reuses it verbatim.
Proof (discrete approximation + limit). For ε > 0 pick finite-range
T, S with transport cost ≤ ε/4 each (exists_finiteRange_map_cost_le). With
μ' = Measure.map T μ, ν' = Measure.map S ν:
W_c(μ,ν) ≤ W_c(μ,μ') + W_c(μ',ν') + W_c(ν',ν)
(wassersteinCostCoupling_triangle ×2, …_comm); the outer terms ≤ ε/4
(wassersteinCostCoupling_map_le); W_c(μ',ν') ≤ dual(μ',ν')
(wassersteinCostCoupling_le_dual_of_finiteRange); dual(μ',ν') ≤ dual(μ,ν) + ε/2 (wassersteinCost_dual_le_add_map). Chain → W_c(μ,ν) ≤ dual(μ,ν) + ε;
ε → 0 (ENNReal.le_of_forall_pos_le_add). The triangle step needs
StandardBorelSpace α (disintegration); consumers instantiate at the Polish
PhaseSpace d.
KR duality at c = dist: wasserstein1 = wasserstein1Coupling. Combines the
hard-direction inequality wassersteinCostCoupling_le_dual with the easy direction
wasserstein1_le_wasserstein1Coupling.
Pushforward of couplings #
These lemmas bridge from coupling-based bounds on initial measures (μ, ν) to
coupling-based bounds on pushed-forward measures (Φ_# μ, Ψ_# ν), which is how
the Dobrushin proof connects characteristic flows back to W₁ growth.
Pushforward of a coupling under a pair of measurable maps is a coupling of the pushed-forward marginals. Pure measure theory; no metric structure needed.
This is the generic α/β shape — the codomain types α', β' can be
arbitrary measurable spaces, not necessarily equal to the domain. This
matters because the characteristic-flow application uses
(Prod.map Φ Ψ) with Φ and Ψ distinct maps; the diagonal
case α' = α, Φ = Ψ is a specialization.
The dual-formula wasserstein1 of the pushed-forward measures is bounded
above by the infimum over couplings of the original measures of the
pushed-forward cost. This is the "iInf trick":
wasserstein1 (Φ_# μ) (Ψ_# ν) ≤ wasserstein1Coupling (Φ_# μ) (Ψ_# ν) (KR easy) = ⨅ π' (coupling of Φ_# μ, Ψ_# ν), ∫⁻ edist dπ' ≤ ⨅ π (coupling of μ, ν), ∫⁻ edist (Φ z.1, Ψ z.2) dπ (push couplings via IsCoupling.map)
Used in the dobrushin proof: applied with Φ, Ψ the characteristic
flows of f, g at time t (or the difference flow), this turns a
W₁-bound on (f_t, g_t) into a coupling-cost bound on (f_0, g_0)
that can be controlled by Gronwall.