Theorem 13.1 -- spectral gap from contracting couplings

Proved

MarkovMixing.contraction_gap

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$ , and let $\rho$ be a metric on $V$ : symmetric, vanishing exactly on the diagonal, and satisfying the triangle inequality. A coupling of the two one-step distributions $P(x,\cdot)$ and $P(y,\cdot)$ is a probability distribution $q$ on pairs whose marginals are those two rows — the joint law of one step of two copies of the chain, from $x$ and from $y$ . Among the eigenvalues of $P$ — the real $\lambda$ admitting a nonzero $f$ with $Pf=\lambda f$ — let $\lambda_\star$ denote the largest absolute value of an eigenvalue different from $1$ , so that $\gamma_\star=1-\lambda_\star$ is the absolute spectral gap.

The theorem (Theorem 13.1 of Levin–Peres–Wilmer) asserts: if for some contraction factor $\theta\ge0$ every pair of states admits a coupling of its one-step distributions that contracts the metric in expectation,

\mathbb E_q\bigl[\rho(X_1,Y_1)\bigr]\le\theta\,\rho(x,y)\qquad\text{for all }x,y,

then $\lambda_\star\le\theta$ — equivalently, $\gamma_\star\ge1-\theta$ .

A contracting coupling forces a spectral gap: the geometric decay of distances under the coupling leaves no room for an eigenfunction to decay slower than $\theta^t$ . This turns the path-coupling constructions of earlier chapters directly into eigenvalue estimates.

Preamble

import Definitions.Def_mm_spectral

Formal statement

namespace MarkovMixing

/-- **Theorem 13.1** (LPW): if for some metric `ρ` on the state space there
is, for every pair of states, a coupling of the one-step distributions that
contracts `ρ` by a factor `θ`, then every eigenvalue other than `1` has
absolute value at most `θ` — that is, `γ⋆ ≥ 1 − θ`. -/
theorem contraction_gap {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (ρ : 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)
    (θ : ℝ) (hθ : 0 ≤ θ)
    (Q : V → V → (V × V → ℝ))
    (hQ : ∀ x y : V, IsCoupling (rowDist P 1 x) (rowDist P 1 y) (Q x y))
    (hcontract : ∀ x y : V, ∑ p : V × V, Q x y p * ρ p.1 p.2 ≤ θ * ρ x y) :
    lambdaStar P ≤ θ := 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 13.1, Theorem 13.1, p. 171

Read-back

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

Let $V$ be a finite set with decidable equality — note that no nonemptiness is assumed, so $V$ may be empty — and let $P$ be a real $V \times V$ matrix that is stochastic: all entries $P_{x,y} \ge 0$ and each row sums to one. The theorem further assumes: a function $\rho : V \times V \to \mathbb{R}$ satisfying the metric axioms — $\rho(x,y) \ge 0$ for all $x,y$ ; $\rho(x,y) = 0$ if and only if $x = y$ ; symmetry $\rho(x,y) = \rho(y,x)$ ; and the triangle inequality $\rho(x,z) \le \rho(x,y) + \rho(y,z)$ ; a real number $\theta$ with $\theta \ge 0$ (note: $\theta$ is not required to be less than $1$ , or even $\le 1$ ); a family $Q$ assigning to each ordered pair of states $(x,y)$ a real-valued function $Q_{x,y}$ on $V \times V$ ; the hypothesis that each $Q_{x,y}$ is a coupling of the two one-step distributions $P(x, \cdot)$ and $P(y, \cdot)$ — meaning $Q_{x,y}$ is a probability distribution on $V \times V$ (all values nonnegative, total sum $1$ ) whose first marginal is row $x$ of $P$ , $\sum_{v} Q_{x,y}(u,v) = P_{x,u}$ for every $u$ , and whose second marginal is row $y$ of $P$ , $\sum_{u} Q_{x,y}(u,v) = P_{y,v}$ for every $v$ (this is a one-step coupling of distributions only; nothing requires $Q$ to fix the diagonal or to define a Markovian coupling of chains); and the contraction hypothesis that for all pairs $x, y$ — including $x = y$ , where it forces the expected distance under $Q_{x,x}$ to be $\le 0$ —

\sum_{(u,v) \in V \times V} Q_{x,y}(u,v)\, \rho(u,v) \;\le\; \theta\, \rho(x,y).

Under all these hypotheses, the conclusion is the single inequality $\lambda^\ast(P) \le \theta$ , where $\lambda^\ast(P)$ is defined as the supremum of the set $\{\,|\lambda| : \lambda \in \mathbb{R},\ \lambda \ne 1,\ \lambda \text{ an eigenvalue of } P\,\}$ , and " $\lambda$ is an eigenvalue of $P$ " means there exists a nonzero function $f : V \to \mathbb{R}$ with $P f = \lambda f$ (a real right eigenvector; complex eigenvalues are not captured by this definition). By Lean's convention the supremum of an empty set of reals is $0$ , so if $P$ has no real eigenvalue other than possibly $1$ , the conclusion degenerates to $0 \le \theta$ , which is already among the hypotheses; likewise when $V$ is empty the coupling hypotheses are vacuously true and the conclusion is again $0 \le \theta$ . The eigenvalue $1$ itself is explicitly excluded from the supremum, but the value $|\lambda| = 1$ can still arise from an eigenvalue $\lambda = -1$ .

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