Proposition 16.2 -- the -reversal chain is far from mixed at
ProvedMarkovMixing.l_reversal_lowerThe -reversal chain shuffles a circular arrangement of cards (an arrangement indexed by ): at each step it picks a starting position and a length uniformly at random and reverses the circular arc of cards from position to position , leaving the rest fixed. Its stationary distribution is uniform. Write for the law after moves from the arrangement , for the total variation distance, and for the chain on cards.
The theorem (Proposition 16.2 of Levin–Peres–Wilmer) asserts: for any family of maximal reversal lengths with and any fixed , evaluating each chain at time gives
Before time the chain is asymptotically as far from uniform as possible, whatever is. The witness is again coupon-collector-flavoured: cards whose neighbourhood no reversal has yet touched retain their original neighbours in the circular order. (In the formal statement the deck sizes are enumerated as , , so that automatically.)
import Definitions.Def_mm_shuffle import Mathlib.Analysis.SpecialFunctions.Log.Basic
namespace MarkovMixing
/-- **Proposition 16.2** (LPW): for the family of `L`-reversal chains with
`1 ≤ L(n) < n/2` and any fixed `0 < ε < 1`, at time
`t(n) = (1−ε)(n/2) log n` the distance to stationarity tends to `1`:
the chain is far from mixed. (States are indexed by `m` with `n = m + 2`.) -/
theorem l_reversal_lower (L : ℕ → ℕ)
(hL : ∀ n : ℕ, 3 ≤ n → 1 ≤ L n ∧ 2 * L n < n)
(ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
Filter.Tendsto
(fun m : ℕ =>
distStationary (groupWalk (lReversalDist (m + 2) (L (m + 2))))
(uniformDist (Equiv.Perm (ZMod (m + 2))))
⌊(1 - ε) * ((m : ℝ) + 2) / 2 * Real.log ((m : ℝ) + 2)⌋₊)
Filter.atTop (nhds 1) := by
sorry
end MarkovMixing