Proposition 8.11 -- random transpositions lower bound

Proved

MarkovMixing.random_transpositions_lower

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

markov-chainsmixing-timesprobability

The random transpositions shuffle of a deck of $n$ cards picks two cards independently and uniformly at random and swaps them: the identity is applied with probability $1/n$ and each transposition with probability $2/n^2$ . Its stationary distribution is uniform. For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ at which $\max_x\|P^t(x,\cdot)-\mathrm{unif}\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance.

The theorem (Proposition 8.11 of Levin–Peres–Wilmer) asserts: for every $n\ge2$ and every $0<\varepsilon<1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\ge\;\frac{n-1}{2}\,\log\!\Bigl(\frac{(1-\varepsilon)\,n}{6}\Bigr).

So order $\tfrac12\,n\log n$ shuffles are necessary. The obstruction is the number of fixed points: until almost every card has been touched at least once — a coupon-collector event taking $\tfrac12 n\log n$ pair draws — the deck has many more cards in their original position than a uniform ordering would.

Preamble

import Definitions.Def_mm_shuffle
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **Proposition 8.11** (LPW): for the random transpositions chain on `n`
cards and `0 < ε < 1`,
`t_mix(ε) ≥ ((n−1)/2) log((1−ε)n/6)`. -/
theorem random_transpositions_lower (n : ℕ) (hn : 2 ≤ n)
    (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    ((n : ℝ) - 1) / 2 * Real.log ((1 - ε) * n / 6) ≤
      (mixingTime (randomTranspositions n)
        (uniformDist (Equiv.Perm (Fin n))) ε : ℝ) := 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 8.2.3, Proposition 8.11, p. 105

Read-back

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

Read-back: `random_transpositions_lower`

For every natural number $n$ with $n \ge 2$ , and every real number $\varepsilon$ with $0 < \varepsilon < 1$ , the following inequality holds:

\frac{n - 1}{2}\,\log\!\left(\frac{(1-\varepsilon)\,n}{6}\right) \;\le\; t_{\mathrm{mix}}(P_n, \varepsilon),

where the right-hand side is a natural number cast to a real, $\log$ is the natural logarithm, subtraction $n-1$ is real subtraction, and the objects are as follows. $P_n$ is the "random transpositions" matrix on the group of permutations of the $n$ -element set $\{0,\dots,n-1\}$ , whose entry in row $a$ , column $b$ equals $\mu(b\,a^{-1})$ , where $\mu$ gives weight $1/n$ to the identity permutation, weight $2/n^2$ to every transposition of two distinct indices, and $0$ to all other permutations (so the entry is $1/n$ when $b = a$ , $2/n^2$ when $b\,a^{-1}$ is a transposition, and $0$ otherwise). The quantity $t_{\mathrm{mix}}(P_n,\varepsilon)$ is the $\varepsilon$ -mixing time toward the uniform distribution $u$ on the permutation group (each of the $n!$ permutations having mass $1/n!$ ): it is the least natural number $t$ (an infimum over naturals) such that

\sup_{x}\; d_{TV}\!\left((P_n^{\,t})(x,\cdot),\, u\right) \;\le\; \varepsilon,

the supremum being over all permutations $x$ as starting states, and $d_{TV}(\mu,\nu)$ being defined as the supremum over all finite subsets $A$ of the state space of $\left|\sum_{x \in A}\mu(x) - \sum_{x\in A}\nu(x)\right|$ (the sup-over-events form of total-variation distance, with no factor $\tfrac12$ ). By the natural-number infimum convention, this mixing time is $0$ if no $t$ meets the threshold. Edge cases worth noting: the right-hand side is always $\ge 0$ , while the left-hand side is negative or zero whenever $(1-\varepsilon)n/6 \le 1$ , i.e. whenever $n \le 6/(1-\varepsilon)$ ; in that regime (which for each fixed $\varepsilon$ includes all $n$ up to some bound, e.g. all $n \le 6$ when $\varepsilon$ is small) the asserted inequality holds trivially, so the statement carries nontrivial content only for $n > 6/(1-\varepsilon)$ . The theorem is a lower bound of order $\tfrac{1}{2} n \log n$ on this $\varepsilon$ -mixing time, stated for every $n \ge 2$ and every $\varepsilon \in (0,1)$ simultaneously.

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

Proposition 8.11 -- random transpositions lower bound

Read-back: random_transpositions_lower

Read-back: `random_transpositions_lower`