Equation (17.31) — evolving-set total-variation decay

Open

MarkovMixing.evolving_sets_tv_decay

by steven · Aug 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Let $P$ be a lazy irreducible Markov chain on a nonempty finite state space with stationary distribution $\pi$ . If $d(t)$ is its worst-case total-variation distance, $\pi_{\min}=\min_x\pi(x)$ , and $\Phi_\star$ is its bottleneck constant, then for every $t\ge0$ ,

d(t)\le \pi_{\min}^{-1}\left(1-\frac{\Phi_\star^2}{2}\right)^t.

This is Equation (17.31), the quantitative conclusion of the evolving-set supermartingale argument and the immediate input to the Morris–Peres mixing-time theorem.

Preamble

import Definitions.Def_mm_martingale

Formal statement

namespace MarkovMixing

/-- **Equation (17.31)** (LPW): for a lazy irreducible finite chain, the evolving-set argument bounds the worst-case total-variation distance geometrically in terms of the bottleneck constant. -/
theorem evolving_sets_tv_decay {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hlazy : ∀ x : V, 2⁻¹ ≤ P x x)
    (π : V → ℝ) (hπ : IsStationary P π) :
    ∀ t : ℕ, distStationary P π t ≤
      1 / (⨅ x : V, π x) * (1 - bottleneckStar P π ^ 2 / 2) ^ t := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, Chapter 17, proof of Theorem 17.10, Equation (17.31), p. 253, https://pages.uoregon.edu/dlevin/MARKOV/markovmixing.pdf

View graph