Proposition 16.2 -- the $L$ -reversal chain is far from mixed at $(1-\varepsilon)\frac n2\log n$

Proved

MarkovMixing.l_reversal_lower

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

The $L$ -reversal chain shuffles a circular arrangement of $n$ cards (an arrangement indexed by $\mathbb Z_n$ ): at each step it picks a starting position $i\in\mathbb Z_n$ and a length $k\in\{0,\dots,L-1\}$ uniformly at random and reverses the circular arc of cards from position $i$ to position $i+k$ , leaving the rest fixed. Its stationary distribution is uniform. Write $P^t(x,\cdot)$ for the law after $t$ moves from the arrangement $x$ , $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ for the total variation distance, and $d_n(t)=\max_x\|P^t(x,\cdot)-\mathrm{unif}\|_{TV}$ for the chain on $n$ cards.

The theorem (Proposition 16.2 of Levin–Peres–Wilmer) asserts: for any family of maximal reversal lengths $L(n)$ with $1\le L(n)<n/2$ and any fixed $0<\varepsilon<1$ , evaluating each chain at time $t_n=\bigl\lfloor(1-\varepsilon)\,\tfrac n2\log n\bigr\rfloor$ gives

d_n(t_n)\;\longrightarrow\;1\qquad(n\to\infty).

Before time $\tfrac n2\log n$ the chain is asymptotically as far from uniform as possible, whatever $L$ 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 $n=m+2$ , $m\to\infty$ , so that $n\ge2$ automatically.)

Preamble

import Definitions.Def_mm_shuffle
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

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

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 16.2.1, Proposition 16.2, p. 222

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Fix a function $L : \mathbb{N} \to \mathbb{N}$ satisfying: for every natural number $n \ge 3$ , both $1 \le L(n)$ and $2\,L(n) < n$ (nothing is assumed about $L(0), L(1), L(2)$ ); and fix a real number $\varepsilon$ with $0 < \varepsilon < 1$ . The theorem asserts that the real sequence $m \mapsto a_m$ converges to $1$ as $m \to \infty$ , where $a_m$ is defined as follows with $n = m+2$ (so $n$ ranges over the integers $\ge 2$ ).

The state space is the group of permutations of $\mathbb{Z}/n\mathbb{Z}$ . Call a permutation $g$ a "circular reversal with parameters $(i,k)$ ", for $i \in \mathbb{Z}/n\mathbb{Z}$ and $k \in \mathbb{N}$ , when for every $j \in \mathbb{Z}/n\mathbb{Z}$ : if the canonical representative of $j - i$ in $\{0,\dots,n-1\}$ is $\le k$ then $g(j) = 2i + k - j$ (arithmetic in $\mathbb{Z}/n\mathbb{Z}$ , with $k$ reduced mod $n$ ), and otherwise $g(j) = j$ — i.e. $g$ reverses the circular arc $\{i, i+1, \dots, i+k\}$ in place and fixes everything else (for $k = 0$ this forces $g$ to be the identity; if $k \ge n-1$ the condition covers the whole circle). The weight function is

\mu_n(g) \;=\; \frac{\#\bigl\{(i,k) \in \mathbb{Z}/n\mathbb{Z} \times \{0,1,\dots,L(n)-1\} \;\bigm|\; g \text{ is the circular reversal with parameters } (i,k)\bigr\}}{n\,L(n)},

counting multiplicity over parameter pairs (in particular the identity receives weight $n/(n\,L(n)) = 1/L(n)$ from the $n$ pairs with $k=0$ ; if $L(n) = 0$ the numerator count is $0$ and the denominator is $0$ , giving $\mu_n \equiv 0$ by the division-by-zero convention — the hypothesis on $L$ rules this out only for $n \ge 3$ ). The transition matrix is the random-walk matrix $P_n(x,y) = \mu_n(y\,x^{-1})$ . The reference distribution is the constant function $\pi_n \equiv 1/n!$ (uniform on the permutation group). The distance between two functions $\mu, \nu$ on the permutation group is $d(\mu,\nu) = \sup_{A}\bigl|\sum_{g \in A}\mu(g) - \sum_{g \in A}\nu(g)\bigr|$ over all finite subsets $A$ (note: no factor $\tfrac12$ ), and the worst-case distance at time $t$ is $d_n(t) = \max_{x} d\bigl(P_n^{t}(x,\cdot),\,\pi_n\bigr)$ over starting states $x$ , using row $x$ of the $t$ -th matrix power. The evaluation time is

t_m \;=\; \Bigl\lfloor (1-\varepsilon)\,\frac{m+2}{2}\,\ln(m+2) \Bigr\rfloor,

a natural number obtained by the nonnegative floor (values below $0$ floor to $0$ , though here the expression is nonnegative), where $\ln$ is the natural logarithm (not base 2). The sequence in question is $a_m = d_{m+2}(t_m)$ , and the assertion is precisely that $a_m \to 1$ (convergence to the value $1$ in the usual topology of $\mathbb{R}$ ; no rate is claimed). The statement carries no hypothesis that $P_n$ is stochastic or that $\pi_n$ is stationary for it, and no claim is made about the mixing time itself — only this limit of distances at the specified times.

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition 16.2 -- the LLL-reversal chain is far from mixed at (1−ε)n2log⁡n(1-\varepsilon)\frac n2\log n(1−ε)2n​logn

Proposition 16.2 -- the $L$ -reversal chain is far from mixed at $(1-\varepsilon)\frac n2\log n$