Proposition 6.10 -- the strong stationary time bound

Proved

MarkovMixing.strong_stationary_bound

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$ . Write $P^t(x,\cdot)$ for the distribution at time $t$ started at $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance, and $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ for the worst-case distance to stationarity. 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 (Proposition 6.10 of Levin–Peres–Wilmer) asserts: if a single stopping rule is a strong stationary time from every starting state, then for every time $t$

d(t)\;\le\;\max_{x\in V}\,\mathbb P_x\{\tau>t\}.

To bound the mixing time of a chain it therefore suffices to construct one strong stationary time and control its tail uniformly in the start.

Preamble

import Definitions.Def_mm_stopping

Formal statement

namespace MarkovMixing

/-- **Proposition 6.10** (LPW): if `τ` is a strong stationary time from every
starting state, then `d(t) ≤ max_x P_x{τ > t}`. -/
theorem strong_stationary_bound {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π)
    (s : ∀ t : ℕ, (Fin (t + 1) → V) → ℝ)
    (hs : ∀ x : V, IsStrongStationaryTime P π x s) (t : ℕ) :
    distStationary P π t ≤ ⨆ x : V, 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, Proposition 6.10, p. 79

Read-back

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

Let $V$ be a finite nonempty type with decidable equality, and let $P$ be a $V \times V$ real matrix assumed to be: 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 of states $x, y$ there is some natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (with $t = 0$ allowed, so $x = y$ is always witnessed by the identity $P^0$ ). Let $\pi : V \to \mathbb{R}$ be assumed stationary for $P$ : $\pi \ge 0$ pointwise, $\sum_y \pi(y) = 1$ , and $\pi P = \pi$ as a row vector. 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 for a start $x$ define

\sigma^x_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, starting from $x$ , of tracing a path that ends at $y$ at time $t$ , not stopping at any earlier time, and stopping at time $t$ under the randomized rule $s$ . The hypothesis on $s$ is that it is a strong stationary time simultaneously for every starting state $x \in V$ ; for each $x$ this means the conjunction of: (i) $0 \le s_t(\omega) \le 1$ for all $t, \omega$ ; (ii) $\sum_{t=0}^{\infty} \sum_y \sigma^x_t(y) = 1$ , where the countable sum over $t$ takes the junk value $0$ if the family is not summable (so summability with sum $1$ is being asserted); and (iii) $\sigma^x_t(y) = \bigl(\sum_z \sigma^x_t(z)\bigr)\,\pi(y)$ for every $t$ and $y$ . Under these hypotheses the theorem asserts, for every natural number $t$ (including $t = 0$ ):

\sup_{x \in V}\; \sup_{A \subseteq V} \left|\, \sum_{y \in A} (P^t)(x,y) - \sum_{y \in A} \pi(y) \,\right| \;\le\; \sup_{x \in V} \left( 1 - \sum_{u=0}^{t} \sum_{y \in V} \sigma^x_u(y) \right).

The left-hand side is the worst-case (over starting states $x$ ) distance at time $t$ between the row $y \mapsto (P^t)(x,y)$ of the $t$ -th matrix power and $\pi$ , where the distance used is the supremum over all finite subsets $A$ of $V$ (the empty set included, contributing $0$ ) of the absolute difference in mass — the supremum of an absolute value, not a half- $\ell^1$ norm. The right-hand side is the supremum over starting states $x$ of one minus the total probability of having stopped at some time $u \le t$ (the inner sum over $u$ runs from $0$ through $t$ inclusive), i.e. the worst-case probability of not yet having stopped by time $t$ ; nothing in the statement constrains this expression to lie in $[0,1]$ beyond what follows from the hypotheses. Both outer suprema are over the finite nonempty index set $V$ . No aperiodicity or reversibility assumption appears.

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