Mixing bounds from path coupling

Proved

MarkovMixing.path_coupling_mixing

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$ with stationary distribution $\pi$ , and suppose the path coupling hypotheses of Theorem 14.6 hold: a connected graph $G$ on $V$ with symmetric edge lengths $\ell\ge1$ , a rate $\alpha>0$ , and for every edge $\{x,y\}$ of $G$ a coupling of $P(x,\cdot),P(y,\cdot)$ contracting the path metric $\rho$ (least total $\ell$ -length of a connecting walk) in expectation by $e^{-\alpha}$ . Write $\mathrm{diam}(V)=\max_{x,y}\rho(x,y)$ for the path-metric diameter, $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ for the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ .

The theorem (Corollary 14.7 of Levin–Peres–Wilmer) asserts:

the distance to stationarity decays geometrically: $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ for every $t$ ;
consequently, for every $0<\varepsilon<1$ , $\;t_{\mathrm{mix}}(\varepsilon)\le\bigl\lceil(-\log\varepsilon+\log\mathrm{diam}(V))/\alpha\bigr\rceil$ .

The proof is one line from path coupling: iterating the one-step contraction bounds $\rho_K(P^t(x,\cdot),\pi)$ by $e^{-\alpha t}\mathrm{diam}(V)$ , and the transportation distance dominates total variation because the path metric is at least $1$ between distinct states.

Preamble

import Definitions.Def_mm_transport
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **Corollary 14.7** (LPW): under the path coupling hypotheses,
`d(t) ≤ e^{-αt} diam(Ω)` and
`t_mix(ε) ≤ ⌈(−log ε + log diam(Ω))/α⌉`. -/
theorem path_coupling_mixing {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary 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) :
    (∀ t : ℕ, distStationary P π t ≤
      Real.exp (-α * t) * ⨆ p : V × V, pathMetric G ℓ p.1 p.2) ∧
    ∀ ε : ℝ, 0 < ε → ε < 1 →
      (mixingTime P π ε : ℝ) ≤
        ⌈(-Real.log ε + Real.log (⨆ p : V × V, pathMetric G ℓ p.1 p.2)) / α⌉₊ := 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, Corollary 14.7, p. 192

Read-back

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

Read-back: path_coupling_mixing

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

$P$ is a stochastic $V \times V$ real matrix (entries $\ge 0$ , rows summing to $1$ ).
$\pi : V \to \mathbb{R}$ is stationary for $P$ : $\pi$ is a probability distribution (pointwise $\ge 0$ , summing to $1$ ) and $\pi P = \pi$ as a row vector.
$G$ is a connected simple graph on $V$ .
$\ell : V \times V \to \mathbb{R}$ satisfies $\ell(x,y) \ge 1$ for every adjacent pair $x \sim y$ , and is symmetric on all pairs.
$\alpha > 0$ is real.
Edge-contraction hypothesis: for every adjacent $x \sim y$ there is a coupling $q$ of the rows $P(x,\cdot)$ and $P(y,\cdot)$ (a probability distribution on $V \times V$ with those two marginals) satisfying $\sum_{(u,v)} q(u,v)\, d_{G,\ell}(u,v) \le e^{-\alpha}\, \ell(x,y)$ , where $d_{G,\ell}(u,v)$ is the real infimum of the $\ell$ -lengths of walks in $G$ from $u$ to $v$ (sum of $\ell$ over the walk's consecutive directed steps; real $\inf$ defaults to $0$ on an empty set, though connectivity keeps it nonempty; $d_{G,\ell}(u,u)$ 's defining set contains $0$ via the trivial walk).

Write $D \;=\; \sup_{(u,v) \in V \times V} d_{G,\ell}(u,v)$ for the supremum of the path metric over all ordered pairs, including diagonal pairs $(u,u)$ ; this is a supremum over a finite nonempty index set. Write $d(t) = \sup_{x \in V} \mathrm{tv}\big(P^t(x,\cdot), \pi\big)$ , where $\mathrm{tv}(\mu,\nu) = \sup_{A \subseteq V} \big| \sum_{x \in A} \mu(x) - \sum_{x \in A} \nu(x) \big|$ (supremum over all finite subsets $A$ , including $\varnothing$ ) is the total-variation-style distance without a factor $\tfrac12$ .

The conclusion is a conjunction of two claims:

Geometric decay to stationarity. For every natural number $t$ (including $t = 0$ ):

d(t) \;\le\; e^{-\alpha t}\, D.

Mixing-time bound. For every real $\varepsilon$ with $0 < \varepsilon < 1$ :

t_{\mathrm{mix}}(\varepsilon) \;\le\; \Big\lceil \frac{-\log \varepsilon + \log D}{\alpha} \Big\rceil_{\!+},

where $t_{\mathrm{mix}}(\varepsilon)$ is the least natural number $t$ with $d(t) \le \varepsilon$ (a natural-number infimum, which equals the junk value $0$ if no such $t$ exists), cast to $\mathbb{R}$ , and $\lceil \cdot \rceil_+$ is the ceiling to a natural number, which clamps any negative argument to $0$ . Note $\log$ is the real logarithm with the convention $\log x = 0$ for $x \le 0$ ; so if $D \le 0$ (conceivable only through the $\inf$ -of-empty-set junk, excluded here by connectivity, or if every pathMetric value were $\le 0$ ) the term $\log D$ would silently be $0$ .

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