Lemma 6.11 -- separation is bounded by the stopping tail

Proved

MarkovMixing.sep_le_stopping_tail

by Shuze Chen · Aug 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

View graph