Lemma 10.1 -- the random target lemma

Proved

MarkovMixing.random_target_lemma

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible Markov chain on a finite state space $V$ with stationary distribution $\pi$ . For states $a$ and $y$ , write $\mathbb E_a(\tau_y)$ for the expected hitting time of $y$ from $a$ — the expected number of steps for the chain started at $a$ to first reach $y$ (formalized, as throughout this series, by the tail-sum $\sum_{t\ge0}\mathbb P_a\{\tau_y>t\}$ ).

The theorem (the Random Target Lemma, Lemma 10.1 of Levin–Peres–Wilmer) asserts that the expected time to hit a $\pi$ -random target does not depend on the starting state: for any two states $a,b$ ,

\sum_{y\in V}\mathbb E_a(\tau_y)\,\pi(y)\;=\;\sum_{y\in V}\mathbb E_b(\tau_y)\,\pi(y).

Choosing the target according to the stationary distribution erases the advantage of any starting position — a surprising exact identity, proved by observing that the quantity is a harmonic function of the start and hence constant for an irreducible chain.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Lemma 10.1, the Random Target Lemma** (LPW): for an irreducible chain
with stationary distribution `π`, the quantity `∑_y E_a(τ_y) π(y)` does not
depend on the starting state `a`. -/
theorem random_target_lemma {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π) (a b : V) :
    ∑ y, expSetHitTime P a {y} * π y = ∑ y, expSetHitTime P b {y} * π 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 10.2, Lemma 10.1, p. 128

Read-back

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

Let $V$ be a finite type with decidable equality, and let $P$ be a $V \times V$ real matrix that is stochastic ( $P(x,y) \ge 0$ for all $x,y$ , and each row sums to $1$ ) and irreducible in the sense that for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (since $P^0$ is the identity, this is automatic when $x = y$ ). Let $\pi : V \to \mathbb{R}$ be a stationary distribution for $P$ : $\pi(x) \ge 0$ for all $x$ , $\sum_{x} \pi(x) = 1$ , and $\pi P = \pi$ as a row vector. For vertices $x, y \in V$ , let $E_x[\tau_y]$ denote the quantity $\sum_{t=0}^{\infty} q_t(x,y)$ , where $q_t(x,y)$ is the total weight $\sum_{\omega} \prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})$ of all paths $\omega : \{0, \dots, t\} \to V$ with $\omega_0 = x$ that avoid $y$ at every step $0 \le i \le t$ , including step $0$ ; probabilistically, $q_t(x,y)$ is the chance that the chain started at $x$ has not visited $y$ by time $t$ , so $E_x[\tau_y] = \sum_{t \ge 0} \Pr_x[\tau_y > t]$ is the expected first hitting time of $y$ , where the hitting time counts time $0$ (in particular $E_y[\tau_y] = 0$ , since a path starting at $y$ fails the avoidance condition at step $0$ , and every term is zero). The infinite sum here is a Lean tsum: if the series fails to converge, the expression takes the junk value $0$ rather than $+\infty$ . The theorem then asserts that for any two vertices $a, b \in V$ (with no assumption that $a \ne b$ ),

\sum_{y \in V} E_a[\tau_y]\, \pi(y) \;=\; \sum_{y \in V} E_b[\tau_y]\, \pi(y),

i.e. the $\pi$ -weighted average over targets $y$ of the expected hitting time of $y$ from the fixed start $a$ equals the same average computed from the start $b$ — the quantity $\sum_{y} E_x[\tau_y] \pi(y)$ does not depend on the starting vertex $x$ . Note that no aperiodicity or reversibility is assumed, and nothing is asserted about the common value itself.

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph