Theorem 5.2 and Corollary 5.3 -- the coupling bound

Proved

MarkovMixing.coupling_bound

by Shuze Chen · Aug 21, 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 write $P^t(x,\cdot)$ for the distribution at time $t$ started at $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance, and $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ for the worst-case distance to stationarity. A Markovian coupling of $P$ is a Markov chain on ordered pairs of states each of whose two coordinates, viewed on its own, moves according to $P$ , and which keeps the two coordinates together once they coincide. For such a coupling started at the pair $(x,y)$ , the coupling time $\tau_{\mathrm{couple}}$ is the first time the pair chain reaches the diagonal $\{(v,v)\}$ — the moment the two copies meet.

Suppose a Markovian coupling $Q_{x,y}$ of $P$ is given for every pair of starting states. The theorem (Theorem 5.2 and Corollary 5.3 of Levin–Peres–Wilmer) asserts:

for every pair $x,y$ and time $t$ , the rows of $P^t$ are close whenever the coupling has probably met: $\bigl\|P^t(x,\cdot)-P^t(y,\cdot)\bigr\|_{TV}\le\mathbb P_{x,y}\{\tau_{\mathrm{couple}}>t\}$ ;
consequently $d(t)\le\max_{x,y}\mathbb P_{x,y}\{\tau_{\mathrm{couple}}>t\}$ .

This is the engine of the coupling method: to bound mixing, build a coupling that meets fast.

Preamble

import Definitions.Def_mm_coupling

Formal statement

namespace MarkovMixing

/-- **Theorem 5.2 and Corollary 5.3** (LPW): if each pair of starting states
carries a Markovian coupling of the chain (staying together after meeting),
then `‖P^t(x,·) − P^t(y,·)‖_TV ≤ P_{x,y}{τ_couple > t}`, and hence
`d(t) ≤ max_{x,y} P_{x,y}{τ_couple > t}`, where `τ_couple` is the hitting
time of the diagonal for the pair chain. -/
theorem coupling_bound {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary P π)
    (Q : V → V → Matrix (V × V) (V × V) ℝ)
    (hQ : ∀ x y : V, IsMarkovianCoupling P (Q x y)) (t : ℕ) :
    (∀ x y : V, tvDist (rowDist P t x) (rowDist P t y) ≤
      setAvoidTailProb (Q x y) (x, y) (pairDiagonal V) t) ∧
    distStationary P π t ≤
      ⨆ p : V × V, setAvoidTailProb (Q p.1 p.2) p (pairDiagonal V) t := 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 5.2, Theorem 5.2 and Corollary 5.3, pp. 64-65

Read-back

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

Let $V$ be a finite, nonempty type with decidable equality, and let $P$ be a real $V \times V$ matrix assumed stochastic, meaning every entry satisfies $P(x,y) \ge 0$ and every row sums to $1$ : $\sum_y P(x,y) = 1$ . Let $\pi : V \to \mathbb{R}$ be assumed stationary for $P$ , meaning $\pi$ is a probability vector ( $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ ) and $\pi P = \pi$ (row-vector–matrix product). Let $Q$ assign to every ordered pair $(x,y) \in V \times V$ a real matrix $Q_{x,y}$ indexed by $(V \times V) \times (V \times V)$ , and assume that for every $x, y$ the matrix $Q_{x,y}$ is a Markovian coupling of $P$ , which here means all four of: (i) $Q_{x,y}$ is stochastic (nonnegative entries, rows summing to $1$ ); (ii) for every current pair $p = (p_1, p_2)$ and every $x' \in V$ , $\sum_{y'} Q_{x,y}\big(p, (x',y')\big) = P(p_1, x')$ (first marginal moves by $P$ from the first coordinate of the current pair); (iii) symmetrically, $\sum_{x'} Q_{x,y}\big(p, (x',y')\big) = P(p_2, y')$ ; (iv) from any diagonal pair $(z,z)$ , the probability of moving to any off-diagonal pair is $0$ (once coupled, the coupling never assigns positive weight off the diagonal in one step). Note that the starting pair $(x,y)$ appears only as the index selecting which coupling matrix is used; conditions (i)–(iv) constrain each $Q_{x,y}$ at all pairs $p$ , not just at $(x,y)$ . Fix also an arbitrary time $t \in \{0, 1, 2, \dots\}$ . Write $D$ for the diagonal $\{(z,z) : z \in V\} \subseteq V \times V$ , and for a stochastic-type matrix $R$ on pairs, a starting pair $p$ , and horizon $t$ , define the diagonal-avoidance mass

A_R(p, t) \;=\; \sum_{\omega} \prod_{i=0}^{t-1} R(\omega_i, \omega_{i+1}),

the sum running over all sequences $\omega : \{0,\dots,t\} \to V \times V$ with $\omega_0 = p$ and $\omega_i \notin D$ for every index $i = 0, \dots, t$ — including $i = 0$ , so if $p$ itself lies on the diagonal (i.e. $x = y$ ) this quantity is $0$ , and at $t = 0$ it is exactly the indicator that $p$ is off the diagonal (the empty product being $1$ ). Write $\mathrm{d_{TV}}(\mu, \nu) = \sup_{A \subseteq V} \big| \sum_{z \in A} \mu(z) - \sum_{z \in A} \nu(z) \big|$ (supremum of the absolute discrepancy over all finite subsets $A$ of $V$ , applied here to arbitrary real-valued vectors), and let $P^t(x, \cdot)$ denote row $x$ of the $t$ -th matrix power of $P$ . The theorem then asserts the conjunction of two claims: (1) for every pair of states $x, y \in V$ ,

\mathrm{d_{TV}}\big(P^t(x,\cdot),\, P^t(y,\cdot)\big) \;\le\; A_{Q_{x,y}}\big((x,y),\, t\big),

i.e. the total-variation distance between the time- $t$ distributions started from $x$ and from $y$ is at most the mass, under the coupling chain $Q_{x,y}$ started at $(x,y)$ , of length- $t$ trajectories that stay off the diagonal at every time from $0$ through $t$ ; and (2)

\sup_{x \in V} \mathrm{d_{TV}}\big(P^t(x,\cdot),\, \pi\big) \;\le\; \sup_{(p_1,p_2) \in V \times V} A_{Q_{p_1,p_2}}\big((p_1,p_2),\, t\big),

i.e. the worst-case (over starting states) total-variation distance to $\pi$ at time $t$ is at most the worst diagonal-avoidance mass over all starting pairs $(p_1, p_2)$ — the supremum on the right ranging over all pairs, including diagonal ones (for which the avoidance mass is $0$ ). The stationarity hypothesis on $\pi$ is used only in claim (2), where $\pi$ appears; no irreducibility or aperiodicity of $P$ is assumed, and the claims hold for the single fixed $t$ quantified in the statement (which is universally quantified, so effectively for all $t \ge 0$ , including $t = 0$ ).

Human review

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

View graph