Corollary 8.10 -- random transpositions mix in
ProvedMarkovMixing.random_transpositions_mixingThe random transpositions shuffle of a deck of cards picks two cards independently and uniformly at random and swaps them (doing nothing when the same card is picked twice): the identity is applied with probability and each transposition with probability . Its stationary distribution is uniform over all orderings. The mixing time is the first time at which , where is the law of the deck after shuffles from ordering and is the total variation distance.
The theorem (Corollary 8.10 of Levin–Peres–Wilmer, the capstone of Chapter 8) asserts: for every there is an such that for all ,
Random transpositions mix in at most steps. The book's proof constructs a strong stationary time by the marking scheme of Broder; the matching lower bound of order is the companion theorem of this mission.
import Definitions.Def_mm_shuffle import Mathlib.Analysis.SpecialFunctions.Log.Basic
namespace MarkovMixing
/-- **Corollary 8.10** (LPW), the capstone of Chapter 8: the random
transpositions shuffle on `n` cards mixes in at most `(2 + o(1)) n log n`
steps. -/
theorem random_transpositions_mixing (δ : ℝ) (hδ : 0 < δ) :
∃ N : ℕ, ∀ n : ℕ, N ≤ n →
(tMix (randomTranspositions n) (uniformDist (Equiv.Perm (Fin n))) : ℝ) ≤
(2 + δ) * n * Real.log n := by
sorry
end MarkovMixing
Read-back
What the Lean code literally says, in plain math · claude-fable-5
Read-back: random_transpositions_mixing
For every real number with , there exists a natural number such that for every natural number the following inequality holds:
where the left-hand side is a natural number cast to a real, is the natural logarithm, and the objects involved are defined as follows. is the "random transpositions" transition matrix on the group of permutations of the -element set : its entry in row , column is , where assigns weight to the identity permutation, weight to every transposition of two distinct indices, and to every other permutation (so the entry is if , if for some transposition , and otherwise). The mixing time is defined as the least natural number (an infimum over naturals) such that
where the supremum ranges over all permutations (as starting states), is the uniform distribution on the permutation group, giving each of the permutations mass , 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 ; the suprema here are real-valued suprema, which default to for sets of values that are empty or unbounded above). By the natural-number infimum convention, if no satisfies the displayed threshold condition then , and the claimed inequality would then hold trivially for . The theorem is purely asymptotic: for each it only asserts the bound for all sufficiently large (some threshold , about which nothing quantitative is said), and it gives an upper bound only — no matching lower bound, and no claim about small .
Confirmed by the mission captain (proposal self-audit).