Null recurrent chains: $P^t(x,y)\to 0$

Proved

MarkovMixing.null_recurrent_convergence

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), and suppose the chain is null recurrent: some state $x_0$ is recurrent — return is certain, $\mathbb P_{x_0}\{\tau^+_{x_0}>t\}\to0$ — but not positive recurrent — the expected return time $\sum_{t\ge0}\mathbb P_{x_0}\{\tau^+_{x_0}>t\}$ diverges. (Simple random walk on $\mathbb Z$ or $\mathbb Z^2$ is the standard example.)

The theorem (Theorem 21.17 of Levin–Peres–Wilmer) asserts: for all states $x,y$ ,

P^t(x,y)\;\longrightarrow\;0\qquad(t\to\infty).

A null recurrent chain visits every state infinitely often, yet at any late fixed time it is nowhere in particular: the mass spreads out and no stationary profile is approached — consistent with this mission's equivalence, since a stationary distribution would force positive recurrence. Together with the positive-recurrent convergence theorem, this completes the trichotomy: transient chains escape, null recurrent chains return but diffuse away, positive recurrent chains converge to their stationary distribution.

Preamble

import Definitions.Def_mm_countable

Formal statement

namespace MarkovMixing

/-- **Theorem 21.17** (LPW): for a null-recurrent irreducible chain on a
countable state space, `P^t(x,y) → 0` for all states `x, y`. -/
theorem null_recurrent_convergence {V : Type*} [Countable V] [DecidableEq V]
    (P : V → V → ℝ) (hP : IsStochasticC P) (hirr : IrreducibleC P)
    (x₀ : V) (hrec : Recurrent P x₀) (hnull : ¬PositiveRecurrent P x₀)
    (x y : V) :
    Filter.Tendsto (fun t => 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.4, Theorem 21.17, Eq. (21.14), p. 283

Read-back

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

Read-back: null_recurrent_convergence

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 nonnegative and each row has sum $1$ in the unconditional (HasSum) sense; (b) $P$ is 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 with $P^{(0)}$ the identity indicator and $P^{(t+1)}(x,y) = \sum'_z P^{(t)}(x,z)P(z,y)$ (a tsum, taking junk value $0$ on any non-summable family); (c) there is a distinguished state $x_0$ that is recurrent in the sense that $R(x_0, t) \to 0$ as $t \to \infty$ , where $R(x_0, t)$ is the total weight

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

of length- $t$ paths from $x_0$ that never revisit $x_0$ (with $R(x_0,0) = 1$ , and junk value $0$ at any $t$ where the path family is non-summable); and (d) $x_0$ is not positive recurrent, i.e. the sequence $t \mapsto R(x_0,t)$ is not summable. Then, for the two further universally quantified states $x, y \in V$ appearing as hypotheses-side binders, the conclusion asserts

\lim_{t \to \infty} P^{(t)}(x, y) = 0,

i.e. the $t$ -step transition value from $x$ to $y$ tends to $0$ as $t \to \infty$ — for every choice of $x$ and $y$ , since they are arbitrary. No rate is asserted, and no claim is made about stationary distributions; the statement is pure pointwise convergence to zero of the iterated-kernel entries.

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

Null recurrent chains: Pt(x,y)→0P^t(x,y)\to 0Pt(x,y)→0

Read-back: null_recurrent_convergence

Null recurrent chains: $P^t(x,y)\to 0$