Section 6.5.3 -- the top-to-random shuffle mixes in $n\log n+cn$ steps

Proved

MarkovMixing.top_to_random_mixing

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

markov-chainsmixing-timesprobability

Consider the top-to-random shuffle of a deck of $n\ge2$ cards: at each step the top card is removed and reinserted at a uniformly random position. Its stationary distribution is uniform over all $n!$ orderings. Write $P^t(x,\cdot)$ for the law of the deck after $t$ shuffles started from the ordering $x$ , $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ for the total variation distance, and $d(t)=\max_x\|P^t(x,\cdot)-\mathrm{unif}\|_{TV}$ for the worst-case distance to uniformity.

The theorem (§6.5.3, display (6.16) of Levin–Peres–Wilmer, the capstone of Chapters 5–6) asserts: for every $\alpha>0$ ,

d\bigl(\lceil n\log n+\alpha n\rceil\bigr)\;\le\;e^{-\alpha}.

After $n\log n$ shuffles plus any linear-in- $n$ margin, the deck is exponentially close to uniform in the margin: $n\log n$ top-to-random shuffles suffice. The proof runs through the strong stationary time of this mission — one shuffle after the original bottom card surfaces — whose tail is controlled by the coupon-collector bounds of Mission I.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **§6.5.3, Eq. (6.16)** (LPW), the capstone of Chapters 5–6: for the
top-to-random shuffle on `n` cards,
`d(⌈n log n + α n⌉) ≤ e^{-α}` for every `α > 0`. -/
theorem top_to_random_mixing (n : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 < α) :
    distStationary (topToRandom n) (uniformDist (Equiv.Perm (Fin n)))
      ⌈(n : ℝ) * Real.log n + α * n⌉₊ ≤ Real.exp (-α) := 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 6.5.3, Eq. (6.16), p. 81

Read-back

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

For every natural number $n$ with $n \ge 2$ and every real number $\alpha > 0$ , the theorem asserts the following inequality. Let $P$ be the "top-to-random" transition matrix on the finite set of permutations of $\{0, 1, \dots, n-1\}$ , whose entry at a pair of permutations $(\sigma, \tau)$ is

P(\sigma, \tau) \;=\; \frac{\#\{\, j \in \{0, \dots, n-1\} \;:\; \tau = \sigma_j \,\}}{n},

where $\sigma_j$ denotes the function sending position $i$ to $\sigma(i+1)$ when $i < j$ , to $\sigma(0)$ when $i = j$ , and to $\sigma(i)$ when $i > j$ — that is, the arrangement obtained from $\sigma$ by removing the entry at position $0$ and reinserting it at position $j$ , with the intervening entries shifted toward position $0$ ; the count is of those $j$ for which $\tau$ agrees pointwise with $\sigma_j$ . Let $u$ denote the constant function on permutations with value $1/n!$ (the reciprocal of the cardinality of the permutation group), and set

t \;=\; \bigl\lceil\, n \ln n + \alpha n \,\bigr\rceil_{\mathbb{N}},

the ceiling of the real number $n \ln n + \alpha n$ taken as a natural number ( $\ln$ is the natural logarithm; the natural-ceiling operation sends any non-positive real to $0$ , though here the argument is positive since $n \ge 2$ and $\alpha > 0$ ). The conclusion is

\sup_{x} \; \sup_{A} \left|\, \sum_{y \in A} (P^{t})(x, y) \;-\; \frac{\#A}{n!} \,\right| \;\le\; e^{-\alpha},

where the outer supremum runs over all starting permutations $x$ , and the inner supremum runs over all finite sets $A$ of permutations (including $A = \emptyset$ , contributing $0$ ), comparing the total mass that the $x$ -th row of the $t$ -th matrix power $P^t$ assigns to $A$ with the mass $\#A / n!$ that the constant density $u$ assigns to $A$ . This double supremum is the development's worst-case "distance to stationarity" at time $t$ : the supremum of an absolute difference of set masses, not a half- $\ell^1$ norm. The statement makes this one claim for the single time $t = \lceil n \ln n + \alpha n \rceil_{\mathbb{N}}$ only; it says nothing about other times, and it does not assert that $u$ is stationary or that $P$ is stochastic — those facts do not appear as hypotheses or conclusions.

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

Section 6.5.3 -- the top-to-random shuffle mixes in nlog⁡n+cnn\log n+cnnlogn+cn steps

Section 6.5.3 -- the top-to-random shuffle mixes in $n\log n+cn$ steps