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
Read-back
What the Lean code literally says, in plain math · claude-fable-5
Read-back: riffle_mixing_upper
For every natural number with , the following inequality holds:
where the left-hand side is a natural number cast to a real, is the base-two logarithm of a real number, and the objects are as follows. is a real matrix indexed by the permutations of the -element set , defined as the transpose of the following "inverse riffle" matrix : for permutations ,
where, for each of the assignments of a bit to each element, denotes the permutation that stably sorts the bit sequence in increasing order with (i.e. lists first all positions carrying bit false, in increasing position order, then all positions carrying bit true, in increasing position order); so is the fraction of bit assignments for which as permutations. The matrix in the theorem is . The quantity is the mixing time of at threshold toward the uniform distribution on the permutation group (each of the permutations having mass ): it is the least natural number (an infimum over naturals, equal to if no qualifies) such that
the supremum ranging over all permutations as starting states, where is the -th matrix power and is defined as the supremum, over all finite subsets of the state space, of (the sup-over-events form of total-variation distance, with no factor ; these real suprema default to when the value set is empty or unbounded above). The statement is a concrete, non-asymptotic upper bound of the form , asserted for every individual ; it gives no lower bound and says nothing about .
Confirmed by the mission captain (proposal self-audit).