Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 8.14 -- the riffle shuffle needs log⁡2n\log_2 nlog2​n shuffles

Proved
MarkovMixing.riffle_mixing_lower

by Shuze Chen · Aug 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmixing-timesprobability

The riffle shuffle (Gilbert–Shannon–Reeds) of a deck of nnn 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 000 move to the top preserving relative order. Its stationary distribution is uniform. For a tolerance ε\varepsilonε, the mixing time tmix(ε)t_{\mathrm{mix}}(\varepsilon)tmix​(ε) is the first ttt with max⁡x∥Pt(x,⋅)−unif∥TV≤ε\max_x\|P^t(x,\cdot)-\mathrm{unif}\|_{TV}\le\varepsilonmaxx​∥Pt(x,⋅)−unif∥TV​≤ε, where ∥μ−ν∥TV=max⁡A∣μ(A)−ν(A)∣\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|∥μ−ν∥TV​=maxA​∣μ(A)−ν(A)∣.

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

tmix(ε)  ≥  (1−δ) log⁡2n.t_{\mathrm{mix}}(\varepsilon)\;\ge\;(1-\delta)\,\log_2 n.tmix​(ε)≥(1−δ)log2​n.

So the upper bound 2log⁡2(4n/3)+12\log_2(4n/3)+12log2​(4n/3)+1 of the companion theorem is sharp up to the constant factor 222: no fixed number of riffle shuffles suffices for all deck sizes, and log⁡2n\log_2 nlog2​n is the true order. The obstruction is counting: ttt shuffles produce at most 2nt2^{nt}2nt equally likely bit-histories, too few to spread mass over n!n!n! orderings until t≳log⁡2nt\gtrsim\log_2 nt≳log2​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

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me