Path coupling (Bubley--Dyer)

Proved

MarkovMixing.path_coupling

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ , and let a connected graph $G$ on $V$ with symmetric edge lengths $\ell\ge1$ be given. The path metric $\rho(x,y)$ is the least total $\ell$ -length of a walk from $x$ to $y$ in $G$ ; a coupling of two distributions is a joint distribution on pairs with those marginals; and the transportation distance $\rho_K(\mu,\nu)$ is the infimum of $\mathbb E_q[\rho]$ over couplings $q$ of $\mu,\nu$ .

The theorem (path coupling, Bubley–Dyer; Theorem 14.6 of Levin–Peres–Wilmer) asserts: if for some rate $\alpha>0$ every edge $\{x,y\}$ of $G$ admits a coupling $q$ of the one-step distributions $P(x,\cdot)$ and $P(y,\cdot)$ contracting in expectation,

\sum_{u,v}q(u,v)\,\rho(u,v)\;\le\;e^{-\alpha}\,\ell(x,y),

then one step of the chain contracts the transportation metric between arbitrary distributions at the same rate:

\rho_K(\mu P,\;\nu P)\;\le\;e^{-\alpha}\,\rho_K(\mu,\nu)\qquad\text{for all distributions }\mu,\nu.

This is the theorem that turns the coupling method into a local computation: contraction needs to be checked only across single edges of any convenient graph structure, and the metric machinery propagates it along paths to all pairs of states — no global coupling construction required.

Preamble

import Definitions.Def_mm_transport
import Mathlib.Analysis.SpecialFunctions.Exp

Formal statement

namespace MarkovMixing

/-- **Theorem 14.6, path coupling** (Bubley–Dyer; LPW): if for every edge
`{x,y}` of a connected graph structure on the state space there is a
coupling of the one-step distributions contracting the path metric by
`e^{-α}`, then one step of the chain contracts the transportation metric of
*arbitrary* distributions by `e^{-α}`. -/
theorem path_coupling {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (G : SimpleGraph V) (hconn : G.Connected)
    (ℓ : V → V → ℝ) (hℓ1 : ∀ x y : V, G.Adj x y → 1 ≤ ℓ x y)
    (hℓsymm : ∀ x y : V, ℓ x y = ℓ y x)
    (α : ℝ) (hα : 0 < α)
    (hedge : ∀ x y : V, G.Adj x y →
      ∃ q : V × V → ℝ, IsCoupling (rowDist P 1 x) (rowDist P 1 y) q ∧
        ∑ p : V × V, q p * pathMetric G ℓ p.1 p.2 ≤ Real.exp (-α) * ℓ x y)
    (μ ν : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) :
    transportDist (pathMetric G ℓ) (Matrix.vecMul μ P) (Matrix.vecMul ν P) ≤
      Real.exp (-α) * transportDist (pathMetric G ℓ) μ ν := 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.2, Theorem 14.6, pp. 191-192

Read-back

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

Read-back: path_coupling

Let $V$ be a finite type with decidable equality. The hypotheses are:

$P$ is a $V \times V$ real matrix that is stochastic: every entry $P(x,y) \ge 0$ and every row sums to $1$ .
$G$ is a simple graph on $V$ that is connected (in particular $V$ is nonempty).
$\ell : V \times V \to \mathbb{R}$ satisfies $\ell(x,y) \ge 1$ whenever $x \sim y$ in $G$ (no condition on non-adjacent pairs), and $\ell$ is symmetric on all pairs: $\ell(x,y) = \ell(y,x)$ for all $x,y$ .
$\alpha$ is a real number with $\alpha > 0$ .
Edge-contraction hypothesis: for every adjacent pair $x \sim y$ in $G$ , there exists $q : V \times V \to \mathbb{R}$ which is a coupling of the two one-step distributions $P(x,\cdot)$ and $P(y,\cdot)$ — i.e. $q \ge 0$ pointwise, $\sum_{(u,v)} q(u,v) = 1$ , $\sum_v q(u,v) = P(x,u)$ for all $u$ , and $\sum_u q(u,v) = P(y,v)$ for all $v$ — such that

\sum_{(u,v) \in V \times V} q(u,v)\, d_{G,\ell}(u,v) \;\le\; e^{-\alpha}\, \ell(x,y).

Here $d_{G,\ell}(u,v)$ is the path (pseudo)metric: the real infimum of $\sum \ell$ over the consecutive directed steps of any walk in $G$ from $u$ to $v$ (walks may repeat vertices; the trivial walk gives $d_{G,\ell}(u,u) \le 0$ -witnessing value $0$ ; since $G$ is connected the defining set is never empty, and each step cost is $\ge 1$ by the hypothesis on adjacent pairs; recall the real $\inf$ of an empty or unbounded-below set would default to $0$ ).

$\mu, \nu : V \to \mathbb{R}$ are probability distributions on $V$ (pointwise $\ge 0$ , each summing to $1$ ).

The conclusion is a single inequality: writing $W(\cdot,\cdot)$ for the transport distance with cost $d_{G,\ell}$ — the real infimum, over couplings $q$ of the two arguments, of $\sum_{(u,v)} d_{G,\ell}(u,v)\, q(u,v)$ , with the convention $\inf \varnothing = 0$ — and writing $\mu P$ for the vector–matrix product $(\mu P)(y) = \sum_x \mu(x) P(x,y)$ (one step of the chain applied to $\mu$ ),

W(\mu P, \;\nu P) \;\le\; e^{-\alpha}\; W(\mu, \nu).

That is: if every edge of $G$ admits a one-step coupling contracting the expected path-distance by the factor $e^{-\alpha}$ , then one step of $P$ contracts the transport distance between any two distributions by that same factor. Note the contraction hypothesis is quantified only over adjacent pairs $x \sim y$ , while the conclusion is for arbitrary distributions; note also that in the edge hypothesis the summand order is $q(u,v)\, d_{G,\ell}(u,v)$ while transportDist uses $d_{G,\ell}(u,v)\, q(u,v)$ — the same real product.

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