Positive recurrence $\iff$ stationary distribution

Proved

MarkovMixing.positive_recurrent_iff_stationary

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible Markov chain on a countable state space $V$ (nonnegative entries, rows summing to one as convergent series, every state reaching every other). A state $x$ is positive recurrent when its expected return time is finite: with $\tau^+_x=\min\{t\ge1:X_t=x\}$ , the tail-sum formula $\mathbb E_x(\tau^+_x)=\sum_{t\ge0}\mathbb P_x\{\tau^+_x>t\}$ converges. A stationary distribution is a nonnegative $\pi$ summing to one with $\sum_x\pi(x)P(x,y)=\pi(y)$ for every $y$ (all as convergent series).

The theorem (Theorem 21.12 of Levin–Peres–Wilmer) asserts: a state is positive recurrent if and only if the chain admits a stationary distribution.

On infinite state spaces, existence of a stationary distribution — automatic in the finite theory of Mission I — becomes a genuine dichotomy: simple random walk on $\mathbb Z$ is recurrent but has infinite expected return times and no stationary distribution, while a positively drifting queue may fail even to be recurrent. The proof constructs $\pi$ from expected visit counts during one excursion from $x$ (normalized by $\mathbb E_x(\tau^+_x)$ , finite exactly under positive recurrence), and conversely reads finiteness of $\mathbb E_x(\tau^+_x)=1/\pi(x)$ off Kac's lemma. Since positive recurrence of one state is thereby equivalent to a state-free condition, it too is a class property.

Preamble

import Definitions.Def_mm_countable

Formal statement

namespace MarkovMixing

/-- **Theorem 21.12** (LPW): an irreducible chain on a countable state space
is positive recurrent if and only if it has a stationary (probability)
distribution. -/
theorem positive_recurrent_iff_stationary {V : Type*} [Countable V]
    [DecidableEq V] (P : V → V → ℝ) (hP : IsStochasticC P)
    (hirr : IrreducibleC P) (x : V) :
    PositiveRecurrent P x ↔ ∃ π : V → ℝ, IsStationaryC 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 21.3, Theorem 21.12, p. 280

Read-back

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

Read-back: positive_recurrent_iff_stationary

Let $V$ be an arbitrary countable type with decidable equality and $P : V \times V \to \mathbb{R}$ a kernel. Assume: (a) $P$ is stochastic — every entry $P(x,y) \ge 0$ and each row $y \mapsto P(x,y)$ has sum $1$ in the unconditional (HasSum) sense; and (b) $P$ is irreducible — for all $x, y \in V$ there exists $t \in \mathbb{N}$ (possibly $0$ ) with $P^{(t)}(x,y) > 0$ , where $P^{(t)}$ is the iterated kernel ( $P^{(0)}$ = identity indicator, $P^{(t+1)}(x,y) = \sum'_z P^{(t)}(x,z)P(z,y)$ , a tsum with junk value $0$ on non-summable families). Then, for the single universally quantified state $x \in V$ , the conclusion is an if and only if:

\Big(\text{the sequence } t \mapsto R(x,t) \text{ is summable}\Big) \iff \Big(\exists\, \pi : V \to \mathbb{R} \text{ stationary for } P\Big).

On the left, $R(x,t)$ is the total weight

R(x,t) = \sum_{\omega : \{0,\dots,t\} \to V}{}' \big[\,\omega_0 = x \wedge \forall i \in \{1,\dots,t\},\ \omega_i \ne x\,\big]\, \prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})

of length- $t$ paths starting at $x$ that never revisit $x$ at times $1,\dots,t$ (a tsum over all such path functions, taking junk value $0$ at any $t$ where the family is non-summable; $R(x,0)=1$ ), and "summable" means unconditional summability of this sequence over $t \in \mathbb{N}$ — this is the definition labeled positive recurrence of $x$ . On the right, "stationary" means: $\pi(x') \ge 0$ for all $x'$ , the family $\pi$ has sum $1$ (HasSum), and for every $y$ the family $x' \mapsto \pi(x')P(x',y)$ has sum exactly $\pi(y)$ . Only existence of a stationary $\pi$ is asserted on the right-hand side — no uniqueness — and the equivalence is stated for each fixed $x$ separately (the right-hand side does not mention $x$ ).

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

Positive recurrence ⟺ \iff⟺ stationary distribution

Read-back: positive_recurrent_iff_stationary

Positive recurrence $\iff$ stationary distribution