Lemma 4.13 -- a walk and its inverse walk mix at the same rate

Proved

MarkovMixing.group_walk_reversal_distance

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

markov-chainsmixing-timesprobability

Let $G$ be a finite group and $\mu$ a probability distribution on $G$ . The random walk on $G$ with increment distribution $\mu$ moves from $a$ to $ha$ with probability $\mu(h)$ : at each step an increment $h\sim\mu$ is drawn and multiplied on the left. Its time reversal is the walk driven by the inverse distribution $\hat\mu(g)=\mu(g^{-1})$ , which undoes $\mu$ -steps. Write $u$ for the uniform distribution on $G$ and $\|\cdot\|_{TV}$ for the total variation distance, $\|\mu-\nu\|_{TV}=\max_{A\subseteq G}|\mu(A)-\nu(A)|$ .

The theorem (Lemma 4.13 of Levin–Peres–Wilmer) asserts that the two walks approach uniformity at exactly the same speed: for every time $t$ , the distribution after $t$ steps started at the identity satisfies

\bigl\|P^t(\mathrm{id},\cdot)-u\bigr\|_{TV}=\bigl\|\hat P^t(\mathrm{id},\cdot)-u\bigr\|_{TV},

where $P$ and $\hat P$ are the transition matrices of the $\mu$ -walk and the $\hat\mu$ -walk. Corollary 4.14 is immediate: a random walk on a group and its time reversal have the same mixing times. For card shuffling this means a shuffle and its inverse shuffle mix equally fast — the reason the riffle shuffle can be analyzed through the easier inverse riffle.

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Lemma 4.13 and Corollary 4.14** (LPW): a random walk on a finite group
and the walk with the inverse increment distribution (its time reversal) are
at the same total variation distance from the uniform distribution at every
time, so in particular they have the same mixing times. -/
theorem group_walk_reversal_distance {G : Type*} [Group G] [Fintype G]
    [DecidableEq G] (μ : G → ℝ) (hμ : IsDist μ) (t : ℕ) :
    tvDist (rowDist (groupWalk μ) t 1) (uniformDist G) =
      tvDist (rowDist (groupWalk (invDist μ)) t 1) (uniformDist G) := 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.6, Lemma 4.13 and Corollary 4.14, pp. 55-56

Read-back

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

Let $G$ be a finite group (necessarily nonempty, since it contains the identity $1$ ), and let $\mu : G \to \mathbb{R}$ be a probability distribution on $G$ , meaning $\mu(g) \ge 0$ for every $g \in G$ and $\sum_{g \in G} \mu(g) = 1$ . Let $t$ be an arbitrary natural number, including $t = 0$ .

Define the random-walk matrix of a function $\nu : G \to \mathbb{R}$ as the $G \times G$ real matrix

P_\nu(a, b) = \nu\bigl(b\,a^{-1}\bigr),

i.e. the entry in row $a$ , column $b$ is $\nu$ evaluated at $b a^{-1}$ (a step from $a$ to $b$ corresponds to left-multiplying $a$ by a group element drawn according to $\nu$ ). Define the reversed distribution $\check\mu : G \to \mathbb{R}$ by $\check\mu(g) = \mu(g^{-1})$ . Let $u : G \to \mathbb{R}$ be the uniform distribution, the constant function $u(g) = |G|^{-1}$ . For two functions $\alpha, \beta : G \to \mathbb{R}$ , define the total-variation-style distance

\operatorname{tv}(\alpha, \beta) = \sup_{A \subseteq G} \Bigl| \sum_{g \in A} \alpha(g) - \sum_{g \in A} \beta(g) \Bigr|,

the supremum over all subsets $A$ of $G$ of the absolute difference of the total masses assigned to $A$ (note there is no factor of $\tfrac12$ in this definition).

The theorem asserts the following equality of real numbers: the distance from the time- $t$ distribution of the $\mu$ -walk started at the identity to the uniform distribution equals the corresponding distance for the walk driven by the reversed distribution $\check\mu$ , that is,

\operatorname{tv}\Bigl( \bigl(P_\mu^{\,t}\bigr)(1, \cdot),\; u \Bigr) \;=\; \operatorname{tv}\Bigl( \bigl(P_{\check\mu}^{\,t}\bigr)(1, \cdot),\; u \Bigr),

where $\bigl(P_\nu^{\,t}\bigr)(1, \cdot)$ denotes row $1$ (the row indexed by the group identity) of the $t$ -th matrix power of $P_\nu$ , viewed as a function $G \to \mathbb{R}$ .

Note the claim is stated only for the starting state $1$ (the identity element), not for arbitrary starting states, and only against the uniform distribution as the reference measure. For $t = 0$ both matrix powers are the identity matrix, so both sides coincide trivially. No irreducibility, aperiodicity, or stationarity assumptions are imposed on the walk — the only hypotheses are that $G$ is a finite group and $\mu$ is a probability distribution.

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