Convergence theorem on countable state spaces

Proved

MarkovMixing.countable_convergence

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible and aperiodic Markov chain on a countable state space $V$ (nonnegative entries, rows summing to one as convergent series; every state reaches every other; the possible return times to each state have greatest common divisor one), and suppose some state is positive recurrent: its expected return time $\mathbb E_x(\tau^+_x)=\sum_{t\ge0}\mathbb P_x\{\tau^+_x>t\}$ is finite. Distances are measured in total variation via the $\ell^1$ formula $\|\mu-\nu\|_{TV}=\tfrac12\sum_y|\mu(y)-\nu(y)|$ .

The theorem (Theorem 21.14 of Levin–Peres–Wilmer) asserts the existence of a distribution $\pi$ on $V$ such that:

$\pi$ is stationary: nonnegative, summing to one, with $\sum_x\pi(x)P(x,y)=\pi(y)$ for all $y$ ;
$\pi$ is the unique stationary distribution of the chain;
from every starting state $x$ , $\;\bigl\|P^t(x,\cdot)-\pi\bigr\|_{TV}\to0$ as $t\to\infty$ .

This is the Convergence Theorem of Mission II transplanted to countable state spaces, with positive recurrence supplying what finiteness gave for free. It is the fundamental theorem of applied Markov chain theory — queues, birth-and-death chains, random walks with drift — and the proof couples two copies of the chain on the product space, using aperiodicity and positive recurrence to force the copies to meet.

Preamble

import Definitions.Def_mm_countable

Formal statement

namespace MarkovMixing

/-- **Theorem 21.14** (LPW): an irreducible, aperiodic, positive recurrent
chain on a countable state space has a unique stationary distribution `π`,
and `‖P^t(x,·) − π‖_TV → 0` for every starting state `x`. -/
theorem countable_convergence {V : Type*} [Countable V] [DecidableEq V]
    (P : V → V → ℝ) (hP : IsStochasticC P) (hirr : IrreducibleC P)
    (hap : AperiodicC P) (x₀ : V) (hpos : PositiveRecurrent P x₀) :
    ∃ π : V → ℝ, IsStationaryC P π ∧
      (∀ π' : V → ℝ, IsStationaryC P π' → π' = π) ∧
      ∀ x : V, Filter.Tendsto
        (fun t => tvDistC (fun y => stepPow P t x y) π)
        Filter.atTop (nhds 0) := 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 21.3, Theorem 21.14, Eq. (21.9), p. 281

Read-back

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

Read-back: countable_convergence

Let $V$ be an arbitrary countable type with decidable equality and let $P : V \times V \to \mathbb{R}$ be a kernel. Assume: (a) $P$ is stochastic in the sense that all entries satisfy $P(x,y) \ge 0$ and each row $y \mapsto P(x,y)$ has sum $1$ in the unconditional (HasSum) sense; (b) $P$ is irreducible in the sense that for all $x, y \in V$ there is some $t \in \mathbb{N}$ (possibly $t = 0$ , which automatically handles $x = y$ ) with $P^{(t)}(x,y) > 0$ , where $P^{(t)}$ is the iterated kernel defined by $P^{(0)} =$ identity indicator and $P^{(t+1)}(x,y) = \sum'_z P^{(t)}(x,z) P(z,y)$ (a tsum, taking the junk value $0$ on any non-summable family); (c) $P$ is aperiodic in the sense that for every $x$ , the natural number $\sup\{d \in \mathbb{N} \mid \forall t \ge 1,\ P^{(t)}(x,x) > 0 \Rightarrow d \mid t\}$ equals exactly $1$ (this $\mathbb{N}$ -supremum is $0$ if the set is unbounded, e.g. when $x$ has no positive return time); and (d) there is a distinguished state $x_0$ that is positive recurrent in the sense that the sequence $t \mapsto R(x_0, t)$ is summable, where $R(x_0,t)$ is the total weight $\sum'_{\omega} [\omega_0 = x_0 \wedge \forall i \in \{1,\dots,t\},\ \omega_i \ne x_0] \prod_{i<t} P(\omega_i, \omega_{i+1})$ of length- $t$ paths from $x_0$ never revisiting $x_0$ (with $R(x_0,0)=1$ , and junk value $0$ if the path family is not summable). The conclusion asserts the existence of a function $\pi : V \to \mathbb{R}$ such that all three of the following hold:

$\pi$ is stationary for $P$ in the sense that $\pi \ge 0$ pointwise, $\pi$ has sum $1$ (unconditional HasSum), and for every $y$ the family $x \mapsto \pi(x)P(x,y)$ has sum exactly $\pi(y)$ ;
$\pi$ is the unique such function: every $\pi' : V \to \mathbb{R}$ satisfying that same stationarity predicate is equal to $\pi$ (as a function);
for every starting state $x \in V$ (not just $x_0$ ),

\lim_{t \to \infty} \tfrac{1}{2}\sum_{y \in V}{}' \big| P^{(t)}(x, y) - \pi(y) \big| = 0,

i.e. the half- $\ell^1$ total-variation quantity between the $t$ -step row $P^{(t)}(x,\cdot)$ and $\pi$ tends to $0$ ; note this quantity itself takes the junk value $0$ at any $t$ where the family $y \mapsto |P^{(t)}(x,y) - \pi(y)|$ fails to be summable.

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