Proposition 8.13 -- the riffle shuffle mixes in
ProvedMarkovMixing.riffle_mixing_upperThe riffle shuffle (Gilbert–Shannon–Reeds) of a deck of cards cuts the deck into two packets and interleaves them; it is formalized as the time reversal of the inverse riffle, in which every card independently receives a uniform bit and the cards labeled are pulled to the top, both packets keeping their relative order. (The reversal is legitimate because the stationary distribution — uniform over the orderings — is preserved, and a walk and its reversal mix at the same speed.) The mixing time is the first time at which , with the total variation distance.
The theorem (Proposition 8.13 of Levin–Peres–Wilmer) asserts: for every deck size ,
Order riffle shuffles suffice — for a standard -card deck this bound is in the famous "about seven shuffles" range. The proof tracks the bits accumulated by the inverse shuffles: once all bit-strings are distinct, the deck is exactly uniform.
import Definitions.Def_mm_shuffle import Mathlib.Analysis.SpecialFunctions.Log.Base
namespace MarkovMixing
/-- **Proposition 8.13** (LPW): for the riffle shuffle on an `n`-card deck,
`t_mix ≤ 2 log₂(4n/3) + 1`. -/
theorem riffle_mixing_upper (n : ℕ) (hn : 2 ≤ n) :
(tMix (riffleShuffle n) (uniformDist (Equiv.Perm (Fin n))) : ℝ) ≤
2 * Real.logb 2 (4 * n / 3) + 1 := by
sorry
end MarkovMixing