Theorem 4.9 -- the Convergence Theorem

Proved

MarkovMixing.convergence_theorem

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

markov-chainsmixing-timesprobability

Let $P$ be the transition matrix of an irreducible and aperiodic Markov chain on a finite state space $V$ — irreducible meaning every state can reach every other in some number of steps, aperiodic meaning the return times to a state have greatest common divisor one — and let $\pi$ be a stationary distribution for $P$ , i.e. $\sum_x\pi(x)P(x,y)=\pi(y)$ for all $y$ . Write $P^t(x,\cdot)$ for the distribution of the chain at time $t$ started at $x$ , and $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance.

The theorem — the Convergence Theorem (Theorem 4.9 of Levin–Peres–Wilmer), the capstone of Chapter 4 — asserts that the chain converges to $\pi$ geometrically fast, uniformly in the starting state: there exist a rate $\alpha\in(0,1)$ and a constant $C>0$ such that

\max_{x\in V}\,\bigl\|P^t(x,\cdot)-\pi\bigr\|_{TV}\;\le\;C\,\alpha^{t}\qquad\text{for every }t\in\mathbb N.

In particular the stationary distribution of an irreducible aperiodic chain is unique and is reached from every starting point, with an error decaying exponentially in time — the statement that gives the mixing time its meaning, and the result all later chapters quantify.

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Theorem 4.9, the Convergence Theorem** (LPW), the capstone of
Chapter 4: an irreducible, aperiodic finite chain converges to its stationary
distribution geometrically fast in total variation:
`max_x ‖P^t(x,·) − π‖_TV ≤ C αᵗ` for some `α ∈ (0,1)` and `C > 0`. -/
theorem convergence_theorem {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hap : Aperiodic P) (π : V → ℝ) (hπ : IsStationary P π) :
    ∃ α : ℝ, α ∈ Set.Ioo (0 : ℝ) 1 ∧ ∃ C : ℝ, 0 < C ∧
      ∀ t : ℕ, distStationary P π t ≤ C * α ^ 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 4.3, Theorem 4.9, p. 52

Read-back

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

Let $V$ be a finite, nonempty set and let $P$ be a $V \times V$ matrix of real numbers that is stochastic: every entry satisfies $P(x,y) \ge 0$ and every row sums to $1$ ( $\sum_y P(x,y) = 1$ for each $x$ ). Assume $P$ is irreducible in the sense that for every ordered pair of states $x, y$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (the exponent $t = 0$ is permitted, so for $x = y$ this holds automatically since $P^0$ is the identity matrix). Assume $P$ is aperiodic in the following custom sense: for every state $x$ , the quantity $\operatorname{per}(x) := \sup\{d \in \mathbb{N} : d \text{ divides every element of } R_x\}$ equals $1$ , where $R_x = \{t \ge 1 : (P^t)(x,x) > 0\}$ is the set of return times of $x$ and the supremum is taken in the natural numbers with the convention that an unbounded set of common divisors yields the junk value $0$ (in particular, if $R_x$ were empty then every natural number would vacuously be a common divisor and $\operatorname{per}(x)$ would be $0 \neq 1$ , so this hypothesis implicitly forces each state to have at least one return time). Let $\pi : V \to \mathbb{R}$ be stationary for $P$ : $\pi$ is a probability distribution ( $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ ) and, as a row vector, $\pi P = \pi$ .

For each time $t \in \mathbb{N}$ , define the distance to stationarity

d(t) = \sup_{x \in V} \; \sup_{A \subseteq V} \Bigl| \sum_{y \in A} (P^t)(x, y) - \sum_{y \in A} \pi(y) \Bigr|,

i.e. the worst case over starting states $x$ of the supremum, over all subsets $A$ of $V$ , of the absolute difference between the mass row $x$ of $P^t$ assigns to $A$ and the mass $\pi$ assigns to $A$ (note this total-variation-style distance carries no factor of $\tfrac12$ ).

The theorem asserts: there exists a real number $\alpha$ with $0 < \alpha < 1$ (strict inequalities on both sides) and there exists a real constant $C > 0$ such that for every natural number $t \ge 0$ ,

d(t) \le C\, \alpha^{\,t}.

The order of quantifiers puts $\alpha$ and $C$ before $t$ : a single pair $(\alpha, C)$ must work uniformly for all times. The bound is required at $t = 0$ as well, where it reads $d(0) \le C$ . Nothing further is claimed about $\alpha$ or $C$ — no relation to eigenvalues, to the size of $V$ , or to any other quantity — and no uniqueness of the stationary distribution $\pi$ is asserted; $\pi$ is simply a given distribution satisfying $\pi P = \pi$ .

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