Lemma 6.13 -- total variation is bounded by separation

Proved

MarkovMixing.tv_le_sep

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ with strictly positive 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

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

for the separation distance at time $t$ from the starting state $x$ .

The theorem (Lemma 6.13 of Levin–Peres–Wilmer) asserts that separation dominates total variation: for every starting state $x$ and every time $t$ ,

\bigl\|P^t(x,\cdot)-\pi\bigr\|_{TV}\;\le\;s_x(t).

Consequently any bound on the separation distance — for instance one obtained from a strong stationary time — is automatically a bound on the total variation distance to stationarity.

Preamble

import Definitions.Def_mm_stopping

Formal statement

namespace MarkovMixing

/-- **Lemma 6.13** (LPW): total variation distance to stationarity is bounded
by the separation distance: `‖P^t(x,·) − π‖_TV ≤ s_x(t)`. -/
theorem tv_le_sep {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary P π) (hpos : ∀ y : V, 0 < π y)
    (x : V) (t : ℕ) :
    tvDist (rowDist P t x) π ≤ sepDist P π x 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.13, p. 80

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 assumed to be stochastic: $P(x,y) \ge 0$ for all $x, y$ , and $\sum_y P(x,y) = 1$ for every row $x$ . Let $\pi : V \to \mathbb{R}$ be assumed stationary for $P$ , meaning $\pi(y) \ge 0$ for all $y$ , $\sum_y \pi(y) = 1$ , and $\pi P = \pi$ as a row vector; assume additionally the strict positivity $\pi(y) > 0$ for every $y \in V$ . Then for every state $x \in V$ and every natural number $t$ (including $t = 0$ , where $P^0$ is the identity matrix), the theorem asserts the inequality

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

The left-hand side is the quantity this development calls the total-variation distance between the time- $t$ distribution started from $x$ (the row $y \mapsto (P^t)(x,y)$ of the $t$ -th matrix power) and $\pi$ : the supremum, over all finite subsets $A$ of $V$ (including $A = \emptyset$ , which contributes $0$ , so this supremum is always $\ge 0$ ), of the absolute difference of the two masses of $A$ — note it is the supremum of an absolute value, not half of an $\ell^1$ norm. The right-hand side is the quantity this development calls the separation distance at time $t$ from $x$ : the supremum over all states $y$ of $1 - (P^t)(x,y)/\pi(y)$ ; under the positivity hypothesis no division by zero occurs in it. Both sides are suprema of real-valued families indexed by finite ranges; in the degenerate case where $V$ is empty, both suprema are over empty families and take the junk value $0$ (and the hypotheses $\sum_y \pi(y) = 1$ and row sums $= 1$ are then unsatisfiable, making the statement vacuous for empty $V$ ). No irreducibility, aperiodicity, or reversibility assumption appears in the statement.

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