Kac's lemma

Proved

MarkovMixing.kac_lemma

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 $\pi$ is a stationary distribution for it: nonnegative, summing to one, with $\sum_x\pi(x)P(x,y)=\pi(y)$ for every $y$ . For a nonempty set of states $S$ and $x\in S$ , the first return time to $S$ is $\tau^+_S=\min\{t\ge1:X_t\in S\}$ , with expectation given by the tail-sum formula $\mathbb E_x(\tau^+_S)=\sum_{t\ge0}\mathbb P_x\{\tau^+_S>t\}$ .

The theorem (Kac's lemma, Lemma 21.13 of Levin–Peres–Wilmer) asserts the exact identity

\sum_{x\in S}\pi(x)\,\mathbb E_x\bigl(\tau^+_S\bigr)\;=\;1,

the series over $S$ converging to exactly $1$ .

Started from stationarity conditioned on being in $S$ , the expected time to return to $S$ is exactly $1/\pi(S)$ — and for a singleton, $\mathbb E_x(\tau^+_x)=1/\pi(x)$ : stationary mass is inverse return time. The identity is a mass-transport double count — every time-step of the stationary chain is the $k$ -th step of exactly one excursion from $S$ — and it is the quantitative link between stationary distributions and return times that drives the positive-recurrence theory of this mission.

Preamble

import Definitions.Def_mm_countable

Formal statement

namespace MarkovMixing

/-- **Lemma 21.13 (Kac)** (LPW): for an irreducible chain with stationary
distribution `π` and any nonempty set `S` of states,
`∑_{x ∈ S} π(x) E_x(τ⁺_S) = 1`. -/
theorem kac_lemma {V : Type*} [Countable V] [DecidableEq V]
    (P : V → V → ℝ) (hP : IsStochasticC P) (hirr : IrreducibleC P)
    (π : V → ℝ) (hπ : IsStationaryC P π) (S : Set V) (hS : S.Nonempty) :
    HasSum (fun x : S => π x.1 * expSetReturnC P x.1 S) 1 := 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, Lemma 21.13, Eq. (21.5), p. 280

Read-back

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

Read-back: kac_lemma

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 — all entries nonnegative and each row has sum $1$ in the unconditional (HasSum) sense; (b) $P$ is irreducible — for all $x, y$ there is $t \in \mathbb{N}$ (with $t = 0$ permitted, which trivializes the diagonal case) such that the iterated-kernel value $P^{(t)}(x,y)$ is strictly positive, where $P^{(t)}$ is defined by $P^{(0)} =$ identity indicator and $P^{(t+1)}(x,y) = \sum'_z P^{(t)}(x,z)P(z,y)$ (tsum, junk value $0$ if non-summable); (c) $\pi : V \to \mathbb{R}$ is stationary — $\pi \ge 0$ pointwise, $\pi$ has sum $1$ (HasSum), and for every $y$ the family $x \mapsto \pi(x)P(x,y)$ has sum exactly $\pi(y)$ ; and (d) $S \subseteq V$ is a nonempty set (not assumed finite). The conclusion asserts that the family indexed by the elements $x$ of $S$ ,

x \;\longmapsto\; \pi(x) \cdot E(x, S), \qquad x \in S,

has sum exactly $1$ in the unconditional (HasSum) sense — so in particular this family is genuinely summable, not merely a tsum evaluating to $1$ . Here $E(x, S)$ is the quantity

E(x, S) = \sum_{t=0}^{\infty}{}' \; T(x, S, t), \qquad T(x, S, t) = \sum_{\omega : \{0,\dots,t\} \to V}{}' \big[\, \omega_0 = x \ \wedge\ \forall i \ne 0,\ \omega_i \notin S \,\big] \prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1}),

i.e. $T(x,S,t)$ is the total path-weight of length- $t$ paths that start at $x$ (which is itself in $S$ ; only indices $i \ge 1$ must avoid $S$ ) and stay outside $S$ at all times $1, \dots, t$ , and $E(x,S)$ sums these tail values over all $t \ge 0$ . Edge-case behavior baked into these totals: $T(x,S,0) = 1$ always (the empty product over the constant path); each inner path-sum is a tsum over all functions $\{0,\dots,t\} \to V$ and takes the junk value $0$ if that family is not summable; and the outer sum over $t$ likewise takes the junk value $0$ if the sequence $t \mapsto T(x,S,t)$ is not summable, in which case the term $\pi(x) E(x,S)$ for that $x$ is $0$ .

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