Proposition 8.14 -- the riffle shuffle needs shuffles
ProvedMarkovMixing.riffle_mixing_lowerThe riffle shuffle (Gilbert–Shannon–Reeds) of a deck of 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 move to the top preserving relative order. Its stationary distribution is uniform. For a tolerance , the mixing time is the first with , where .
The theorem (Proposition 8.14 of Levin–Peres–Wilmer) asserts: for any fixed tolerances and margin there is an such that for all ,
So the upper bound of the companion theorem is sharp up to the constant factor : no fixed number of riffle shuffles suffices for all deck sizes, and is the true order. The obstruction is counting: shuffles produce at most equally likely bit-histories, too few to spread mass over orderings until .
import Definitions.Def_mm_shuffle import Mathlib.Analysis.SpecialFunctions.Log.Base
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