Proposition 8.14 -- the riffle shuffle needs $\log_2 n$ shuffles

Proved

MarkovMixing.riffle_mixing_lower

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

markov-chainsmixing-timesprobability

The riffle shuffle (Gilbert–Shannon–Reeds) of a deck of $n$ cards cuts the deck into two packets and interleaves them; formally it is the time reversal of the inverse riffle, in which each card independently receives a uniform bit and the cards labeled $0$ move to the top preserving relative order. Its stationary distribution is uniform. For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_x\|P^t(x,\cdot)-\mathrm{unif}\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ .

The theorem (Proposition 8.14 of Levin–Peres–Wilmer) asserts: for any fixed tolerances $0<\varepsilon<1$ and margin $0<\delta<1$ there is an $N$ such that for all $n\ge N$ ,

t_{\mathrm{mix}}(\varepsilon)\;\ge\;(1-\delta)\,\log_2 n.

So the upper bound $2\log_2(4n/3)+1$ of the companion theorem is sharp up to the constant factor $2$ : no fixed number of riffle shuffles suffices for all deck sizes, and $\log_2 n$ is the true order. The obstruction is counting: $t$ shuffles produce at most $2^{nt}$ equally likely bit-histories, too few to spread mass over $n!$ orderings until $t\gtrsim\log_2 n$ .

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Proposition 8.14** (LPW): for the riffle shuffle on an `n`-card deck
and fixed `0 < ε, δ < 1`, for sufficiently large `n`,
`t_mix(ε) ≥ (1 − δ) log₂ n`. -/
theorem riffle_mixing_lower (ε δ : ℝ) (hε : 0 < ε) (hε1 : ε < 1)
    (hδ : 0 < δ) (hδ1 : δ < 1) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      (1 - δ) * Real.logb 2 n ≤
        (mixingTime (riffleShuffle 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.3.3, Proposition 8.14, p. 110

Read-back

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

For every pair of real numbers $\varepsilon$ and $\delta$ with $0 < \varepsilon < 1$ and $0 < \delta < 1$ , there exists a natural number $N$ such that for every natural number $n \ge N$ ,

(1-\delta)\,\log_2 n \;\le\; t_{\mathrm{mix}}^{(n)}(\varepsilon),

where the right-hand side is a natural number (cast to a real) defined as follows. The state space is the group $S_n$ of permutations of $\{0,\dots,n-1\}$ . The "riffle shuffle" transition matrix $P_n$ is defined entrywise by

P_n(x,y) \;=\; \frac{1}{2^n}\,\#\Bigl\{\, b : \{0,\dots,n-1\} \to \{0,1\} \;\Bigm|\; \forall q,\; x(q) = y\bigl(\sigma_b(q)\bigr) \,\Bigr\},

where, for each bit-string $b$ , $\sigma_b$ is the (stable) sorting permutation of the tuple $q \mapsto b(y(q))$ — i.e. the permutation produced by the library's sorting operation, which rearranges positions so that the composed tuple is monotone (with $0 < 1$ ), breaking ties by position. (The matrix is defined by this counting formula alone; the statement carries no hypothesis that $P_n$ is stochastic, irreducible, or anything else.) The reference distribution is the constant function $\pi_n(g) = 1/n!$ on $S_n$ (the uniform distribution). The total-variation-style distance between two functions $\mu,\nu : S_n \to \mathbb{R}$ used here is $d(\mu,\nu) = \sup_{A \subseteq S_n} \bigl|\sum_{g\in A}\mu(g) - \sum_{g\in A}\nu(g)\bigr|$ , the supremum over all finite subsets $A$ of the absolute difference of the sums (note: no factor $\tfrac12$ ). The worst-case distance to $\pi_n$ at time $t$ is $d_n(t) = \max_{x \in S_n} d\bigl(P_n^t(x,\cdot),\, \pi_n\bigr)$ , where $P_n^t(x,\cdot)$ is row $x$ of the $t$ -th matrix power. Finally,

t_{\mathrm{mix}}^{(n)}(\varepsilon) \;=\; \inf\{\, t \in \mathbb{N} \mid d_n(t) \le \varepsilon \,\},

with the convention (from the infimum over natural numbers) that this equals $0$ when no such $t$ exists. Here $\log_2 n$ denotes the real base-2 logarithm of $n$ (with the convention $\log_2 0 = 0$ , though the claim is only about all sufficiently large $n$ : the threshold $N$ may depend on $\varepsilon$ and $\delta$ , and may be chosen arbitrarily large). The asserted inequality is non-strict ( $\le$ ), and the conclusion is a lower bound: $(1-\delta)\log_2 n$ is at most the mixing quantity.

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.14 -- the riffle shuffle needs log⁡2n\log_2 nlog2​n shuffles

Proposition 8.14 -- the riffle shuffle needs $\log_2 n$ shuffles