Separation vs total variation: $s(2t)\le 1-(1-\bar d(t))^2$

Proved

MarkovMixing.sep_tv_relation

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ with stationary distribution $\pi$ , reversible with respect to it (detailed balance: $\pi(x)P(x,y)=\pi(y)P(y,x)$ ). Two ways of measuring distance from stationarity at time $t$ : the maximal separation distance

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

which is small only when every transition probability has caught up with its stationary value, and the worst pairwise total variation distance $\bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{TV}$ , with $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ (Mission II).

The theorem (Lemma 19.3, Aldous–Diaconis; Levin–Peres–Wilmer) asserts: for every time $t$ ,

s(2t)\;\le\;1-\bigl(1-\bar d(t)\bigr)^2.

Separation at twice the time is controlled by total variation at the original time: once the chain is well mixed in total variation, running it for the same time again brings every individual transition probability up to nearly its stationary value. The proof writes $P^{2t}(x,y)$ as a sum over midpoints, applies reversibility to fold the two halves, and uses Cauchy–Schwarz. In this mission the lemma is the bridge from cover-time estimates (which control $\bar d$ for the lamplighter chain) to the separation bounds in the lamplighter mixing theorem.

Preamble

import Definitions.Def_mm_cutoff

Formal statement

namespace MarkovMixing

/-- **Lemma 19.3** (Aldous–Diaconis; LPW): for a reversible chain, the
separation and total variation distances satisfy
`s(2t) ≤ 1 − (1 − d̄(t))²`. -/
theorem sep_tv_relation {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π) (hrev : DetailedBalance P π)
    (t : ℕ) :
    sepSup P π (2 * t) ≤ 1 - (1 - distPairs P t) ^ 2 := 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 19.2, Lemma 19.3 (Aldous--Diaconis), Eq. (19.8), p. 260

Read-back

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

Read-back: sep_tv_relation

Let $V$ be a finite nonempty type with decidable equality, let $P$ be a real $V \times V$ matrix assumed stochastic (all entries $\ge 0$ , each row summing to $1$ ), assumed irreducible (for every ordered pair $x,y$ there is some $t \in \mathbb{N}$ — possibly $t = 0$ , where $P^0 = I$ — with $(P^t)(x,y) > 0$ ), and let $\pi : V \to \mathbb{R}$ be assumed stationary for $P$ ( $\pi \ge 0$ pointwise, $\sum_x \pi(x) = 1$ , and $\pi P = \pi$ as row vectors) and in detailed balance with $P$ ( $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$ ). Then for every natural number $t$ (including $t = 0$ ), the theorem asserts the single inequality

s(2t) \;\le\; 1 - \bigl(1 - \bar d(t)\bigr)^2,

where the two sides unfold as follows. The left side is the separation supremum at time $2t$ :

s(2t) \;=\; \sup_{x \in V}\, \sup_{y \in V}\, \Bigl(1 - \frac{(P^{2t})(x,y)}{\pi(y)}\Bigr),

a real supremum over all ordered pairs of states of one minus the ratio of the $(x,y)$ entry of the $2t$ -th matrix power to $\pi(y)$ ; the division is Lean's total division, so any $y$ with $\pi(y) = 0$ makes its term equal to $1 - 0 = 1$ (irreducibility and stationarity do not by themselves appear in the formula — the junk convention is part of what is literally asserted). The right side uses the maximal pairwise total-variation-type distance at time $t$ :

\bar d(t) \;=\; \sup_{(x,x') \in V \times V}\; \sup_{A \subseteq V} \Bigl|\sum_{y \in A}(P^t)(x,y) - \sum_{y \in A}(P^t)(x',y)\Bigr|,

the supremum over all ordered pairs of starting states of the supremum over all subsets $A$ of $V$ of the absolute difference between the masses that the two rows of $P^t$ assign to $A$ (diagonal pairs $x = x'$ are included and contribute $0$ ). The inequality is non-strict, compares the separation quantity at the doubled time $2t$ against $1 - (1-\bar d(t))^2$ at time $t$ , and is asserted for each fixed $t$ (no limit is taken); at $t = 0$ both powers are the identity matrix.

Human review

Endorsed by Community (Bot) · Aug 22, 2026
Endorsed by Shuze Chen · Aug 22, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Separation vs total variation: s(2t)≤1−(1−dˉ(t))2s(2t)\le 1-(1-\bar d(t))^2s(2t)≤1−(1−dˉ(t))2

Read-back: sep_tv_relation

Separation vs total variation: $s(2t)\le 1-(1-\bar d(t))^2$