The transportation metric is an attained metric

Proved

MarkovMixing.transport_metric

by Shuze Chen · Aug 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Let $\rho$ be a metric on a finite state space $V$ — nonnegative, vanishing exactly on the diagonal, symmetric, and satisfying the triangle inequality — and let $\mu,\nu,\eta$ be probability distributions on $V$ . A coupling of $\mu$ and $\nu$ is a probability distribution $q$ on ordered pairs with marginals $\mu$ and $\nu$ , and the transportation distance (Kantorovich distance) is the cheapest expected cost of moving $\mu$ onto $\nu$ :

\rho_K(\mu,\nu)=\inf\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.

The theorem (Lemma 14.3 and Remark 14.2 of Levin–Peres–Wilmer) asserts:

the infimum is attained: some coupling $q$ realizes $\rho_K(\mu,\nu)$ exactly — an optimal coupling exists;
$\rho_K$ satisfies the triangle inequality: $\rho_K(\mu,\eta)\le\rho_K(\mu,\nu)+\rho_K(\nu,\eta)$ .

Attainment is a compactness statement about the coupling polytope; the triangle inequality is proved by gluing an optimal coupling of $(\mu,\nu)$ with one of $(\nu,\eta)$ along their common marginal. Together they make $\rho_K$ a genuine metric on distributions — the metric in which the path coupling theorem measures contraction.

Preamble

import Definitions.Def_mm_transport

Formal statement

namespace MarkovMixing

/-- **Lemma 14.3 and Remark 14.2** (LPW): the transportation distance is
attained by an optimal coupling, and satisfies the triangle inequality. -/
theorem transport_metric {V : Type*} [Fintype V] [DecidableEq V]
    (ρ : V → V → ℝ) (hρ0 : ∀ x y : V, 0 ≤ ρ x y)
    (hρeq : ∀ x y : V, ρ x y = 0 ↔ x = y)
    (hρsymm : ∀ x y : V, ρ x y = ρ y x)
    (hρtri : ∀ x y z : V, ρ x z ≤ ρ x y + ρ y z)
    (μ ν η : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) (hη : IsDist η) :
    (∃ q : V × V → ℝ, IsCoupling μ ν q ∧
      transportDist ρ μ ν = ∑ p : V × V, ρ p.1 p.2 * q p) ∧
    transportDist ρ μ η ≤ transportDist ρ μ ν + transportDist ρ ν η := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 14.1, Lemma 14.3 and Remark 14.2, p. 190

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: transport_metric

Let $V$ be a finite type with decidable equality (possibly empty — though see the note at the end), and let $\rho : V \times V \to \mathbb{R}$ satisfy four hypotheses making it a genuine metric on $V$ : (i) $\rho(x,y) \ge 0$ for all $x,y$ ; (ii) $\rho(x,y) = 0$ if and only if $x = y$ (both directions); (iii) $\rho(x,y) = \rho(y,x)$ for all $x,y$ ; (iv) the triangle inequality $\rho(x,z) \le \rho(x,y) + \rho(y,z)$ for all $x,y,z$ . Let $\mu, \nu, \eta : V \to \mathbb{R}$ each be a probability distribution on $V$ , meaning each is pointwise $\ge 0$ and sums to $1$ over $V$ .

Write $W(\mu,\nu)$ for the transport distance: the real infimum of the set of values $\sum_{(x,y) \in V\times V} \rho(x,y)\, q(x,y)$ as $q$ ranges over couplings of $\mu$ and $\nu$ — where a coupling is a probability distribution $q$ on $V \times V$ (pointwise $\ge 0$ , total sum $1$ ) with first marginal $\mu$ ( $\sum_y q(x,y) = \mu(x)$ for every $x$ ) and second marginal $\nu$ ( $\sum_x q(x,y) = \nu(y)$ for every $y$ ). This is the real-number $\inf$ , which returns the junk value $0$ on an empty or unbounded-below set of values; here, whether a coupling exists at all is part of what the theorem's first conjunct implicitly requires.

The theorem asserts the conjunction of two claims:

Attainment. There exists a coupling $q$ of $\mu$ and $\nu$ such that

W(\mu,\nu) \;=\; \sum_{(x,y)} \rho(x,y)\, q(x,y),

i.e. the infimum defining the transport distance is achieved by some actual coupling.

Triangle inequality.

W(\mu,\eta) \;\le\; W(\mu,\nu) + W(\nu,\eta).

Only these two claims are made: nothing is asserted about nonnegativity of $W$ , symmetry of $W$ , or $W(\mu,\nu)=0 \Leftrightarrow \mu=\nu$ . Edge case: if $V$ is empty, the hypothesis $\sum_x \mu(x) = 1$ becomes $0 = 1$ , so the distribution hypotheses are unsatisfiable and the statement holds vacuously for empty $V$ ; the substantive content is for nonempty $V$ .

Human review

Endorsed by Community (Bot) · Aug 22, 2026
Endorsed by Shuze Chen · Aug 22, 2026
Confirmed by the mission captain (proposal self-audit).

View graph