Pólya's theorem

Proved

MarkovMixing.polya_recurrence

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

markov-chainsmixing-timesprobability

Simple random walk on the lattice $\mathbb Z^d$ moves from a point to one of its $2d$ nearest neighbours (one coordinate changed by $\pm1$ ) uniformly at random. The walk is recurrent when return to the starting point is certain — the probability of no return by time $t$ , $\mathbb P_0\{\tau^+_0>t\}$ , tends to $0$ — and transient when with positive probability it never returns.

The theorem (Pólya's theorem; §21.2, Examples 21.8–21.9 of Levin–Peres–Wilmer — the capstone of Chapters 20–21) asserts:

in dimensions $d=1$ and $d=2$ , the walk is recurrent;
in every dimension $d\ge3$ , the walk is transient.

"A drunk man will find his way home, but a drunk bird may get lost forever." The dichotomy is decided by the Green's-function criterion of this mission: the return probabilities obey $P^{2t}(0,0)\asymp t^{-d/2}$ (a local central-limit estimate, by Stirling's formula in low dimension), and $\sum_tt^{-d/2}$ diverges exactly for $d\le2$ . Pólya's 1921 theorem inaugurated the dimension-dependent study of random walks; formalizing the transient half in particular requires genuinely quantitative control of $d$ -dimensional return probabilities.

Preamble

import Definitions.Def_mm_countable

Formal statement

namespace MarkovMixing

/-- **Pólya's theorem** (LPW §21.2, Examples 21.8 and 21.9), the capstone of
Chapters 20–21: simple random walk on `ℤ^d` is recurrent in dimensions
`d ≤ 2` and transient in dimensions `d ≥ 3`. -/
theorem polya_recurrence :
    (∀ d : ℕ, 1 ≤ d → d ≤ 2 → Recurrent (srwZ d) (fun _ => 0)) ∧
    (∀ d : ℕ, 3 ≤ d → ¬Recurrent (srwZ d) (fun _ => 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.2, Examples 21.8-21.9 (Pólya's theorem), p. 278

Read-back

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

Read-back: polya_recurrence

This theorem has no hypotheses and no free variables; it is a conjunction of two universally quantified claims about the concrete kernel $\mathrm{srw}_d$ on the state space $\mathbb{Z}^d$ (functions from a $d$ -element index type to $\mathbb{Z}$ ), defined by $\mathrm{srw}_d(x,y) = \frac{1}{2d}$ when $y$ differs from $x$ by exactly $\pm 1$ in a single coordinate and agrees with $x$ in all other coordinates, and $\mathrm{srw}_d(x,y) = 0$ otherwise. "Recurrent at the origin" abbreviates the following: the sequence $t \mapsto R(t)$ tends to $0$ as $t \to \infty$ , where

R(t) = \sum_{\omega : \{0,\dots,t\} \to \mathbb{Z}^d}{}' \big[\,\omega_0 = \mathbf{0} \ \wedge\ \forall i \in \{1,\dots,t\},\ \omega_i \ne \mathbf{0}\,\big]\, \prod_{i=0}^{t-1} \mathrm{srw}_d(\omega_i, \omega_{i+1})

is the total weight of length- $t$ paths starting at the origin $\mathbf{0}$ (the all-zeros configuration) that never revisit the origin at times $1,\dots,t$ ; the sum over paths is a tsum, taking the junk value $0$ at any $t$ where the path family is not summable, and $R(0) = 1$ (empty product). The two claims are:

for every natural number $d$ with $1 \le d \le 2$ (i.e. $d \in \{1, 2\}$ ), the walk $\mathrm{srw}_d$ is recurrent at the origin in the above sense ( $R(t) \to 0$ );
for every natural number $d$ with $d \ge 3$ , the walk $\mathrm{srw}_d$ is not recurrent at the origin — i.e. the sequence $R(t)$ does not converge to $0$ .

Note that no stochasticity, irreducibility, or other structural hypotheses appear — the claims are about the explicit kernel $\mathrm{srw}_d$ only, and the case $d = 0$ is asserted by neither conjunct.

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