Lemma 4.11 -- comparing $d(t)$ and $\bar d(t)$

Proved

MarkovMixing.dist_le_distPairs

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

markov-chainsmixing-timesprobability

Let $P$ be the transition matrix of a Markov chain on a finite state space $V$ with stationary distribution $\pi$ (that is, $\sum_x\pi(x)P(x,y)=\pi(y)$ for all $y$ ), and write $P^t(x,\cdot)$ for the distribution of the chain at time $t$ started at $x$ , and $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance. Chapter 4 of Levin–Peres–Wilmer measures convergence by two quantities: the worst-case distance to stationarity and the worst pairwise distance,

d(t)=\max_{x\in V}\bigl\|P^t(x,\cdot)-\pi\bigr\|_{TV},\qquad \bar d(t)=\max_{x,y\in V}\bigl\|P^t(x,\cdot)-P^t(y,\cdot)\bigr\|_{TV}.

The theorem (Lemma 4.11) asserts that for every time $t$ these are equivalent up to a factor of two:

d(t)\;\le\;\bar d(t)\;\le\;2\,d(t).

The left inequality holds because $\pi$ is an average of the rows $P^t(y,\cdot)$ ; the right is the triangle inequality through $\pi$ . The point of $\bar d$ is that, unlike $d$ , it is submultiplicative — the subject of the companion lemma.

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Lemma 4.11** (LPW): `d(t) ≤ d̄(t) ≤ 2 d(t)`. -/
theorem dist_le_distPairs {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary P π) (t : ℕ) :
    distStationary P π t ≤ distPairs P t ∧
    distPairs P t ≤ 2 * distStationary P π 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 4.4, Lemma 4.11, p. 53

Read-back

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

Let $V$ be a finite, nonempty type with decidable equality, let $P$ be a $V \times V$ real matrix assumed stochastic (every entry satisfies $0 \le P(x,y)$ and every row sums to $1$ : $\forall x,\ \sum_y P(x,y) = 1$ ), let $\pi : V \to \mathbb{R}$ be assumed stationary for $P$ — meaning $\pi$ is a probability distribution ( $\forall x,\ 0 \le \pi(x)$ and $\sum_x \pi(x) = 1$ ) and the row-vector–matrix product satisfies $\pi P = \pi$ , i.e. $\sum_x \pi(x)\,P(x,y) = \pi(y)$ for every $y$ — and let $t$ be an arbitrary natural number (including $t = 0$ , where $P^0$ is the identity matrix and each row is a point mass). The statement uses the custom total-variation quantity

\mathrm{tvDist}(\mu,\nu) \;=\; \sup_{A \subseteq V}\ \Bigl|\sum_{x \in A}\mu(x) - \sum_{x \in A}\nu(x)\Bigr|

(a supremum over all subsets of the finite type $V$ , with no factor $\tfrac12$ ), and the two derived quantities

d(t) \;=\; \sup_{x \in V}\ \mathrm{tvDist}\bigl(P^t(x,\cdot\,),\ \pi\bigr), \qquad \bar d(t) \;=\; \sup_{(x,y) \in V \times V}\ \mathrm{tvDist}\bigl(P^t(x,\cdot\,),\ P^t(y,\cdot\,)\bigr),

where $P^t(x,\cdot\,)$ denotes the function $y \mapsto (P^t)(x,y)$ , the $x$ -th row of the $t$ -th matrix power of $P$ . All suprema are taken in $\mathbb{R}$ (with the convention that an empty or unbounded supremum equals $0$ ; here the index sets are nonempty and finite over subsets/points of $V$ , so under the hypotheses they are genuine maxima). The theorem asserts the conjunction of two non-strict inequalities:

d(t) \;\le\; \bar d(t) \qquad \text{and} \qquad \bar d(t) \;\le\; 2\, d(t).

Both inequalities are claimed for every single $t$ , under the stated stochasticity and stationarity hypotheses; nothing further (irreducibility, aperiodicity, etc.) is assumed.

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

Lemma 4.11 -- comparing d(t)d(t)d(t) and dˉ(t)\bar d(t)dˉ(t)

Lemma 4.11 -- comparing $d(t)$ and $\bar d(t)$