Proposition 7.13 -- lower bound for the lazy hypercube walk

Proved

MarkovMixing.hypercube_lower_bound

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

markov-chainsmixing-timesprobability

The lazy random walk on the $n$ -dimensional hypercube has state space $\{0,1\}^n$ ; at each step it stays put with probability $\tfrac12$ and otherwise flips a uniformly chosen coordinate. Its stationary distribution is uniform. Write $P^t(x,\cdot)$ for the law at time $t$ started at $x$ , $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ for the total variation distance, and $d(t)=\max_x\|P^t(x,\cdot)-\mathrm{unif}\|_{TV}$ .

The theorem (Proposition 7.13 of Levin–Peres–Wilmer) asserts: for every $n\ge2$ , every $\alpha>0$ , and every integer time

t\;\le\;\tfrac12\,n\log n-\alpha n,\qquad\text{one has}\qquad d(t)\;\ge\;1-8\,e^{\,1-2\alpha}.

So slightly before time $\tfrac12 n\log n$ the walk is still essentially unmixed. The distinguishing statistic is the Hamming weight: started at the all-ones vertex, the number of ones stays measurably above its equilibrium level until the last slow coordinates have been refreshed. Combined with the matching upper bound, this pins the hypercube's mixing time at $\tfrac12 n\log n$ to leading order.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Proposition 7.13** (LPW): for the lazy random walk on the
`n`-dimensional hypercube, `d(½ n log n − α n) ≥ 1 − 8 e^{-2α+1}`.  (Stated
for every integer time `t ≤ ½ n log n − α n`.) -/
theorem hypercube_lower_bound (n : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 < α)
    (t : ℕ) (ht : (t : ℝ) ≤ 2⁻¹ * n * Real.log n - α * n) :
    1 - 8 * Real.exp (1 - 2 * α) ≤
      distStationary (hypercubeWalk n) (uniformDist (Fin n → ZMod 2)) t := 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 7.3.1, Proposition 7.13, p. 95

Read-back

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

Fix a natural number $n$ with $n \ge 2$ , a real number $\alpha > 0$ , and a natural number $t$ (so $t \ge 0$ ) satisfying $t \le \tfrac{1}{2}\, n \ln n - \alpha n$ , where $\ln$ is the natural logarithm; note that if $\tfrac{1}{2} n \ln n - \alpha n < 0$ (e.g. $\alpha \ge \tfrac{1}{2}\ln n$ ) this hypothesis is unsatisfiable and the theorem is vacuous for such parameters. The chain under consideration, written here $P_n$ , is the lazy random walk on the $n$ -dimensional hypercube, obtained by unfolding the definitions as follows: the state space is $\{0,1\}^n$ (functions from an $n$ -element index set to $\mathbb{Z}/2$ ); the underlying graph joins $x$ and $y$ exactly when they differ and there is a single coordinate $j$ with all other coordinates equal and $y_j = x_j \pm 1$ — which in $\mathbb{Z}/2$ means precisely that $x$ and $y$ differ in exactly one coordinate, so every vertex has degree $n$ ; the simple walk moves from $x$ to each neighbor with probability $1/(\text{degree of }x) = 1/n$ and to non-neighbors with probability $0$ ; and the lazy version is $\tfrac{1}{2}I + \tfrac{1}{2}(\text{simple walk})$ , i.e. stay put with probability $\tfrac12$ , otherwise flip one uniformly chosen coordinate. Let $u$ denote the uniform function on $\{0,1\}^n$ , assigning every state the value $2^{-n}$ (the reciprocal of the cardinality of the state space). Define the worst-case distance to $u$ at time $t$ as

d(t) \;=\; \sup_{x \in \{0,1\}^n}\; d_{\mathrm{TV}}\bigl(P_n^t(x, \cdot),\; u\bigr),

where $P_n^t(x,\cdot)$ is row $x$ of the $t$ -th matrix power (with $P_n^0 = I$ ), and the total-variation distance between two real-valued functions $\mu,\nu$ on the state space is itself defined as $d_{\mathrm{TV}}(\mu,\nu) = \sup_{A} \bigl|\sum_{x\in A}\mu(x) - \sum_{x \in A}\nu(x)\bigr|$ , the supremum over all subsets $A$ of the (finite) state space, with no factor of $\tfrac12$ . The theorem's conclusion is the single non-strict inequality

1 - 8\,e^{\,1 - 2\alpha} \;\le\; d(t).

Note that the left-hand side is negative unless $\alpha \ge \tfrac{1 + \ln 8}{2} \approx 1.54$ , so for smaller $\alpha$ the conclusion is trivially true (since $d(t) \ge 0$ ); the bound is informative only for large $\alpha$ , and the hypotheses require nothing linking $\alpha$ to $n$ beyond the constraint on $t$ above.

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