Proposition 8.11 -- random transpositions lower bound
ProvedMarkovMixing.random_transpositions_lowermarkov-chainsmixing-timesprobability
The random transpositions shuffle of a deck of cards picks two cards independently and uniformly at random and swaps them: the identity is applied with probability and each transposition with probability . Its stationary distribution is uniform. For a tolerance , the mixing time is the first at which , where is the total variation distance.
The theorem (Proposition 8.11 of Levin–Peres–Wilmer) asserts: for every and every ,
So order shuffles are necessary. The obstruction is the number of fixed points: until almost every card has been touched at least once — a coupon-collector event taking pair draws — the deck has many more cards in their original position than a uniform ordering would.
Preamble
import Definitions.Def_mm_shuffle import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
namespace MarkovMixing
/-- **Proposition 8.11** (LPW): for the random transpositions chain on `n`
cards and `0 < ε < 1`,
`t_mix(ε) ≥ ((n−1)/2) log((1−ε)n/6)`. -/
theorem random_transpositions_lower (n : ℕ) (hn : 2 ≤ n)
(ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
((n : ℝ) - 1) / 2 * Real.log ((1 - ε) * n / 6) ≤
(mixingTime (randomTranspositions 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.2.3, Proposition 8.11, p. 105