Lemma 6.11 -- separation is bounded by the stopping tail

Proved

MarkovMixing.sep_le_stopping_tail

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$ , and let $x$ be a starting state. The separation distance at time $t$ from $x$ is

s_x(t)=\max_{y\in V}\Bigl(1-\frac{P^t(x,y)}{\pi(y)}\Bigr),

which measures how far the time- $t$ distribution is from covering $\pi$ state by state ( $s_x(t)=0$ exactly when $P^t(x,y)\ge\pi(y)$ everywhere). A strong stationary time $\tau$ for the chain started at $x$ is a randomized stopping rule that stops in finite time almost surely, with the stopped state distributed exactly as $\pi$ and independent of the stopping time.

The theorem (Lemma 6.11 of Levin–Peres–Wilmer) asserts: for every strong stationary time $\tau$ and every time $t$ ,

s_x(t)\;\le\;\mathbb P_x\{\tau>t\}.

The tail of any strong stationary time controls the separation distance — the reason constructing such times yields mixing upper bounds.

Preamble

import Definitions.Def_mm_stopping

Formal statement

namespace MarkovMixing

/-- **Lemma 6.11** (LPW): if `τ` is a strong stationary time for the chain
started at `x`, then the separation distance satisfies
`s_x(t) ≤ P_x{τ > t}`. -/
theorem sep_le_stopping_tail {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π)
    (s : ∀ t : ℕ, (Fin (t + 1) → V) → ℝ) (x : V)
    (hs : IsStrongStationaryTime P π x s) (t : ℕ) :
    sepDist P π x t ≤ stopTailProb P x s t := 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 6.4, Lemma 6.11, p. 79

Read-back

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

Let $V$ be a finite type (possibly empty) with decidable equality, and let $P$ be a $V \times V$ matrix of real numbers such that: $P$ is stochastic, meaning $P(x,y) \ge 0$ for all $x,y$ and every row sums to $1$ ; and $P$ is irreducible in the sense that for every pair of states $x, y$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (note $t = 0$ is allowed, so the case $y = x$ is always witnessed by $P^0 = I$ ). Let $\pi : V \to \mathbb{R}$ be a stationary distribution for $P$ , meaning $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ , and $\pi P = \pi$ as a row vector. Let $x$ be a state and let $s$ be a family assigning to each time $t$ and each trajectory $\omega = (\omega_0,\dots,\omega_t) \in V^{t+1}$ a real number $s_t(\omega)$ , and define for each $t$ and $y \in V$

\sigma_t(y) \;=\; \sum_{\substack{\omega : \{0,\dots,t\} \to V \\ \omega_0 = x,\ \omega_t = y}} \left(\prod_{i=0}^{t-1} P(\omega_i,\omega_{i+1})\right)\left(\prod_{u=0}^{t-1}\bigl(1 - s_u(\omega_0,\dots,\omega_u)\bigr)\right) s_t(\omega),

the probability of following a path from $x$ ending at $y$ at time $t$ , not stopping before $t$ , and stopping at $t$ under the randomized rule $s$ . Assume $s$ is a strong stationary time for $(P, \pi)$ started at $x$ , which by definition is the conjunction of: (i) $0 \le s_t(\omega) \le 1$ for every $t$ and $\omega$ ; (ii) $\sum_{t=0}^{\infty} \sum_{y \in V} \sigma_t(y) = 1$ , the countable sum over $t$ being interpreted with the convention that a non-summable family sums to $0$ ; and (iii) $\sigma_t(y) = \bigl(\sum_{z} \sigma_t(z)\bigr)\,\pi(y)$ for every $t$ and $y$ . Then the conclusion is: for every natural number $t$ (including $t = 0$ ),

\sup_{y \in V}\left(1 - \frac{(P^t)(x,y)}{\pi(y)}\right) \;\le\; 1 - \sum_{u=0}^{t} \sum_{y \in V} \sigma_u(y).

The left-hand side is the separation distance at time $t$ from the start $x$ : a supremum over all states $y$ , with the conventions that division by $\pi(y) = 0$ yields the junk value $0$ (so such a $y$ contributes the term $1$ ), and that if $V$ is empty the supremum over the empty family of reals takes the junk value $0$ . The right-hand side is one minus the total probability of having stopped at some time $u \le t$ (the sum over $u$ runs over $u = 0, 1, \dots, t$ inclusive), i.e. the probability that the rule has not yet stopped by time $t$ ; nothing in the statement forces this quantity to lie in $[0,1]$ — it is exactly the expression $1 - \sum_{u \le t}\sum_y \sigma_u(y)$ .

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