Biased walk cutoff at $\beta^{-1}n$ with window $\sqrt n$

Proved

MarkovMixing.biased_walk_cutoff

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

markov-chainsmixing-timesprobability

The lazy biased random walk on the segment $\{0,1,\dots,n\}$ with up-probability $p>\tfrac12$ moves as follows: from an interior state, hold with probability $\tfrac12$ , step up with probability $p/2$ , step down with probability $(1-p)/2$ ; at each endpoint, hold with probability $\tfrac12$ and step inward with probability $\tfrac12$ . Write $\beta=p-\tfrac12$ for the bias, $\pi_n$ for the stationary distribution (which weights the top of the segment geometrically), and $d_n(t)=\max_x\|P^t_n(x,\cdot)-\pi_n\|_{TV}$ for the worst-case total variation distance. A family has a cutoff at $t_n$ with window $w_n$ when $w_n/t_n\to0$ and $d_n(\lfloor t_n+\alpha w_n\rfloor)$ tends (liminf/limsup over $n$ ) to $1$ as $\alpha\to-\infty$ and to $0$ as $\alpha\to+\infty$ .

The theorem (Theorem 18.2 of Levin–Peres–Wilmer) asserts: the family has a cutoff at

t_n=\beta^{-1}n\qquad\text{with window}\qquad w_n=\sqrt n.

The mechanism is transparent: the walk must travel distance $n$ against a deterministic drift of speed $\beta$ , taking time $\beta^{-1}n$ , with diffusive fluctuations of order $\sqrt n$ around it — the cutoff time is a law of large numbers and the window a central limit theorem. This is the simplest chain exhibiting a genuine cutoff, and the book's warm-up for the hypercube.

Preamble

import Definitions.Def_mm_cutoff
import Mathlib.Analysis.SpecialFunctions.Sqrt

Formal statement

namespace MarkovMixing

/-- **Theorem 18.2** (LPW): the lazy biased random walk on `{0,…,n}` with
bias `β = p − 1/2 > 0` has a cutoff at `β⁻¹ n` with a window of order
`√n`. -/
theorem biased_walk_cutoff (p : ℝ) (hp : 1 / 2 < p) (hp1 : p < 1)
    (π : ∀ n : ℕ, Fin (n + 1) → ℝ)
    (hπ : ∀ n, 0 < n → IsStationary (biasedSegmentWalk n p) (π n)) :
    HasCutoffWindow (fun n => biasedSegmentWalk n p) π
      (fun n => (p - 1 / 2)⁻¹ * n) (fun n => Real.sqrt 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 18.2.1, Theorem 18.2, p. 249

Read-back

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

Read-back: `biased_walk_cutoff`

Fix a real number $p$ with $\tfrac12 < p$ and $p < 1$ . For each $n \in \mathbb{N}$ let $P_n$ denote the $(n+1)\times(n+1)$ real matrix on the state space $\{0,1,\dots,n\}$ defined entrywise, with the branches evaluated in this order, by:

Row $k = 0$ : $P_n(0,0) = \tfrac12$ ; $P_n(0,l) = \tfrac12$ if $l$ has value $1$ ; all other entries $0$ . (Both boundary moves here have probability $\tfrac12$ , not involving $p$ . When $n = 0$ the state space is the single point $0$ , this branch still applies, and the unique row sums to $\tfrac12$ only, so $P_0$ is not stochastic.)
Row $k = n$ (when $n \ge 1$ , since the $k=0$ branch takes precedence): $P_n(n,n) = \tfrac12$ ; $P_n(n,l) = \tfrac12$ if $l + 1 = n$ (i.e. $l = n-1$ ); all other entries $0$ . (Again probability $\tfrac12$ , independent of $p$ .)
Interior rows $0 < k < n$ : $P_n(k,k) = \tfrac12$ , $P_n(k,k+1) = \tfrac{p}{2}$ , $P_n(k,k-1) = \tfrac{1-p}{2}$ , and $0$ otherwise.

Also given is a family of functions $\pi_n : \{0,\dots,n\} \to \mathbb{R}$ (arbitrary real-valued, one for each $n$ ), subject to the single hypothesis: for every $n$ with $0 < n$ , $\pi_n$ is stationary for $P_n$ , meaning $\pi_n$ is a probability vector (all entries $\ge 0$ , entries summing to $1$ ) and the row-vector product satisfies $\pi_n P_n = \pi_n$ . The function $\pi_0$ is completely unconstrained (it need not be a distribution, nor nonnegative).

Define, for each $n$ and each time $t \in \mathbb{N}$ , the worst-case distance to $\pi_n$ :

d_n(t) \;=\; \sup_{x \in \{0,\dots,n\}} \; \sup_{A \subseteq \{0,\dots,n\}} \Bigl|\, \sum_{y \in A} (P_n^{\,t})(x,y) \;-\; \sum_{y \in A} \pi_n(y) \Bigr|,

where both suprema are over the finite state space and its (finitely many) subsets, and $P_n^0$ is the identity matrix. (This is the total-variation-style distance used throughout; nothing here requires the rows of $P_n^t$ or $\pi_n$ to be probability vectors.)

Writing $t(n) = (p - \tfrac12)^{-1} \cdot n$ and $w(n) = \sqrt{n}$ , the theorem asserts the conjunction of the following three statements (this is the definition of the "cutoff window" predicate being claimed):

Window is negligible: $\dfrac{w(n)}{t(n)} = \dfrac{\sqrt{n}}{(p-\tfrac12)^{-1} n} \longrightarrow 0$ as $n \to \infty$ . (At $n = 0$ this quotient is $0/0 = 0$ under the total-division convention; being a limit at infinity, finitely many terms are irrelevant.)
Lower window limit: the function of a real parameter $\alpha$ ,

\alpha \;\longmapsto\; \liminf_{n \to \infty} \; d_n\bigl(\lfloor t(n) + \alpha\, w(n) \rfloor_{\mathbb{N}}\bigr),

tends to $1$ as $\alpha \to -\infty$ . Here $\lfloor \cdot \rfloor_{\mathbb{N}}$ is the natural-number floor, which sends every negative real to $0$ ; so for a fixed $\alpha < 0$ and small $n$ the evaluation time may be clamped to $0$ .

Upper window limit: the function

\alpha \;\longmapsto\; \limsup_{n \to \infty} \; d_n\bigl(\lfloor t(n) + \alpha\, w(n) \rfloor_{\mathbb{N}}\bigr)

tends to $0$ as $\alpha \to +\infty$ .

Nothing else is asserted: in particular there is no claim about mixing times, no claim of stationarity for $\pi_0$ , and the statement quantifies the three limits over the entire family $n \in \mathbb{N}$ , including the degenerate index $n = 0$ (which, entering only through limits at infinity, cannot affect their truth).

Human review

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

View graph

Biased walk cutoff at β−1n\beta^{-1}nβ−1n with window n\sqrt nn​

Read-back: biased_walk_cutoff

Biased walk cutoff at $\beta^{-1}n$ with window $\sqrt n$

Read-back: `biased_walk_cutoff`