Lemma 4.12 -- submultiplicativity of $\bar d$

Proved

MarkovMixing.distPairs_submultiplicative

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

markov-chainsmixing-timesprobability

Let $P$ be any stochastic matrix on a finite state space $V$ (nonnegative entries, rows summing to one), write $P^t(x,\cdot)$ for the row of the $t$ -th matrix power — the distribution at time $t$ of the chain started at $x$ — and let

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

be the worst pairwise total variation distance between two copies of the chain at time $t$ .

The theorem (Lemma 4.12 of Levin–Peres–Wilmer) asserts that $\bar d$ is submultiplicative:

\bar d(s+t)\;\le\;\bar d(s)\cdot\bar d(t)\qquad\text{for all }s,t\in\mathbb N.

No irreducibility or aperiodicity is needed. Combined with the comparison $d\le\bar d\le 2d$ to the distance to stationarity, submultiplicativity is what makes distances decay geometrically past the mixing time, and hence what makes the mixing time a meaningful single parameter of a chain.

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Lemma 4.12** (LPW): `d̄` is submultiplicative:
`d̄(s + t) ≤ d̄(s) · d̄(t)`. -/
theorem distPairs_submultiplicative {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (P : Matrix V V ℝ) (hP : IsStochastic P) (s t : ℕ) :
    distPairs P (s + t) ≤ distPairs P s * distPairs 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.12, p. 54

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$ ), and let $s$ and $t$ be arbitrary natural numbers — both may be $0$ , in which case the corresponding matrix power $P^0$ is the identity matrix. Define, using 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$ , carrying no factor $\tfrac12$ ), the pairwise-row quantity

\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 $z \mapsto (P^t)(x,z)$ , the $x$ -th row of the $t$ -th power of $P$ ; the pairs range over all of $V \times V$ , including the diagonal pairs $(x,x)$ . All suprema are taken in $\mathbb{R}$ with the convention that an empty or unbounded supremum equals $0$ (here the index sets are finite and nonempty since $V$ is nonempty, so they are genuine maxima). The theorem asserts the single non-strict inequality

\bar d(s + t) \;\le\; \bar d(s)\,\cdot\,\bar d(t),

for every such $s$ and $t$ , assuming only that $P$ is stochastic — no stationary distribution, irreducibility, or aperiodicity is assumed, and the right-hand side is a product (not a sum) of the two quantities.

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.12 -- submultiplicativity of dˉ\bar ddˉ

Lemma 4.12 -- submultiplicativity of $\bar d$