The recurrence dichotomy via Green's functions

Proved

MarkovMixing.recurrence_dichotomy

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 with each row summing to one as a convergent series, and every state reaching every other at some time. For a state $x$ , the first return time is $\tau^+_x=\min\{t\ge1:X_t=x\}$ ; the state is recurrent when return is certain, $\mathbb P_x\{\tau^+_x>t\}\to0$ as $t\to\infty$ , and transient otherwise. The Green's function at $x$ is the expected number of visits to $x$ ,

G(x,x)=\sum_{t=0}^{\infty}P^t(x,x).

The theorem (Proposition 21.3 of Levin–Peres–Wilmer) asserts:

a state $x$ is recurrent if and only if its Green's series diverges — equivalently, transience is exactly summability of the return probabilities $P^t(x,x)$ ;
recurrence is a class property: if one state of the irreducible chain is recurrent, every state is.

The equivalence comes from the renewal structure: the number of returns to $x$ is geometric with success probability $\mathbb P_x\{\tau^+_x<\infty\}$ , so its expectation $G(x,x)$ is finite exactly when return is uncertain. This dichotomy is the standard tool for deciding recurrence — Pólya's theorem, the goal of this mission, is proved by estimating the series $\sum_tP^t(0,0)\asymp\sum_tt^{-d/2}$ for the walk on $\mathbb Z^d$ .

Preamble

import Definitions.Def_mm_countable

Formal statement

namespace MarkovMixing

/-- **Proposition 21.3** (LPW): for an irreducible chain on a countable
state space, a state is recurrent if and only if its Green's function
`G(x,x) = ∑_t P^t(x,x)` diverges, and recurrence of one state implies
recurrence of all states. -/
theorem recurrence_dichotomy {V : Type*} [Countable V] [DecidableEq V]
    (P : V → V → ℝ) (hP : IsStochasticC P) (hirr : IrreducibleC P) (x : V) :
    (Recurrent P x ↔ ¬Summable fun t => stepPow P t x x) ∧
    (Recurrent P x → ∀ y : V, Recurrent P y) := 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.1, Proposition 21.3, p. 276

Read-back

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

Read-back: recurrence_dichotomy

Let $V$ be an arbitrary countable type with decidable equality and $P : V \times V \to \mathbb{R}$ a kernel. Assume $P$ is stochastic (every entry nonnegative; each row has sum $1$ in the unconditional HasSum sense) and irreducible (for all $x, y$ there exists $t \in \mathbb{N}$ , possibly $0$ , 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 with junk value $0$ on non-summable families). For the single universally quantified state $x \in V$ , the conclusion is the conjunction of two claims. Writing $R(x,t)$ for 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 from $x$ never revisiting $x$ (tsum over all such path functions, junk value $0$ if non-summable; $R(x,0) = 1$ ), and calling a state $z$ recurrent when $R(z,t) \to 0$ as $t \to \infty$ , the two claims are:

Green's-function criterion, as an iff: $x$ is recurrent if and only if the sequence $t \mapsto P^{(t)}(x,x)$ of diagonal iterated-kernel values is not summable (note the $t = 0$ term of this sequence is $P^{(0)}(x,x) = 1$ ; the criterion is about summability of the sequence itself, not about the value of any tsum);
Solidarity: if $x$ is recurrent, then every state $y \in V$ is recurrent (in the same $R(y,t) \to 0$ sense).

The dichotomy direction is exact: recurrence is equated with non-summability of the return sequence, so equivalently, $x$ fails to be recurrent iff $\sum_t P^{(t)}(x,x)$ is a genuinely summable series.

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