$t_{\mathrm{mix}}(G^\ast)\asymp t_{\mathrm{cov}}(G)$ for lamplighter chains

Proved

MarkovMixing.lamplighter_mixing

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

markov-chainsmixing-timesprobability

Let $(G_n)$ be any sequence of connected graphs with $|V_n|\to\infty$ . The base walk on $G_n$ is the lazy simple random walk (hold with probability $\tfrac12$ , else move to a uniform neighbour); its cover time $t_{\mathrm{cov}}(G_n)$ is the worst, over starting vertices, expected time to have visited every vertex (Mission VI). The lamplighter chain $G_n^\ast$ has states (lamp configuration in $\{0,1\}^{V_n}$ , lamplighter position); one step randomizes the lamp at the current position, moves the lamplighter one base-walk step, and randomizes the lamp at the new position; its stationary distribution is uniform lamps times the base walk's stationary distribution. The mixing time $t_{\mathrm{mix}}(G_n^\ast)$ is the first $t$ at which the worst-case total variation distance $\max_s\|P^t(s,\cdot)-\pi\|_{TV}$ drops to $1/4$ , with $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ .

The theorem (Theorem 19.2 of Levin–Peres–Wilmer) asserts: there are constants $c_1,c_2>0$ such that for all sufficiently large $n$ ,

c_1\,t_{\mathrm{cov}}(G_n)\;\le\;t_{\mathrm{mix}}(G_n^\ast)\;\le\;c_2\,t_{\mathrm{cov}}(G_n).

The lamp configuration looks uniform only once (essentially) every lamp has been touched, so the lamplighter mixes exactly when the base walk has covered the graph — the cleanest theorem converting cover times into mixing times. The upper bound couples two lamplighters after a cover-time's worth of steps; the lower bound shows that before a constant fraction of the cover time, the set of unvisited lamps betrays the starting configuration (via the separation–total-variation relation of this mission).

Preamble

import Definitions.Def_mm_cutoff

Formal statement

namespace MarkovMixing

/-- **Theorem 19.2** (LPW): the mixing time of the lamplighter chain is
comparable to the cover time of the underlying lazy walk: there are
constants `c₁, c₂ > 0` such that for all sufficiently large `n`,
`c₁ t_cov(G_n) ≤ t_mix(G_n⁎) ≤ c₂ t_cov(G_n)`. -/
theorem lamplighter_mixing {Vf : ℕ → Type*} [∀ n, Fintype (Vf n)]
    [∀ n, DecidableEq (Vf n)] [∀ n, Nonempty (Vf n)]
    (G : ∀ n, SimpleGraph (Vf n)) [∀ n, DecidableRel (G n).Adj]
    (hconn : ∀ n, (G n).Connected)
    (hcard : Filter.Tendsto (fun n => Fintype.card (Vf n))
      Filter.atTop Filter.atTop) :
    ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      c₁ * coverTimeMax (lazy (graphWalk (G n))) ≤
        (tMix (lamplighter (G n)) (lamplighterStationary (G n)) : ℝ) ∧
      (tMix (lamplighter (G n)) (lamplighterStationary (G n)) : ℝ) ≤
        c₂ * coverTimeMax (lazy (graphWalk (G 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 19.3, Theorem 19.2, Eq. (19.7), p. 260

Read-back

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

Read-back: lamplighter_mixing

Fix, for every natural number $n$ , a finite nonempty vertex type $\mathcal{V}_n$ (decidable equality) and a simple graph $G_n$ on $\mathcal{V}_n$ (decidable adjacency), and assume: every $G_n$ is connected, and $|\mathcal{V}_n| \to \infty$ as $n \to \infty$ . (No other relation between $n$ and the graphs is assumed; in particular $|\mathcal{V}_n|$ need not equal $n$ .) Let $Q_n = \tfrac12 I + \tfrac12 W_n$ denote the lazy simple random walk on $G_n$ , where $W_n(x,y) = (\deg_{G_n} x)^{-1}$ if $x \sim y$ and $0$ otherwise ( $0^{-1} = 0$ for an isolated vertex, though connectivity with $|\mathcal{V}_n| \ge 2$ precludes those; for $|\mathcal{V}_n| = 1$ the one-point graph is connected and $Q_n = \tfrac12 I$ ). Define two quantities.

Cover time. $t_{\mathrm{cov}}(Q_n) = \sup_{x} \sum_{t=0}^{\infty} c_x(t)$ , where $c_x(t)$ is the sum, over all length- $t$ trajectories $\omega = (\omega_0,\dots,\omega_t)$ with $\omega_0 = x$ that miss at least one vertex (some $y$ with $\omega_i \ne y$ for all $i \le t$ ), of the product $\prod_{i<t} Q_n(\omega_i,\omega_{i+1})$ — i.e. the probability the walk started at $x$ has not yet visited every vertex by time $t$ . The infinite sum is Lean's tsum: if the family is not summable the value is the junk value $0$ ; the outer supremum is a real supremum over the finite nonempty vertex set.

Lamplighter mixing time. Let $L_n$ be the lamplighter chain on states $(f, v)$ with $f : \mathcal{V}_n \to \{\text{off},\text{on}\}$ a lamp configuration and $v$ a walker position: from $(f,v)$ , a transition to $(g,u)$ has probability $Q_n(v,v)/2 = 1/4$ if $u = v$ and $g$ agrees with $f$ off $v$ (the lamp at $v$ unconstrained), probability $Q_n(v,u)/4$ if $u \ne v$ and $g$ agrees with $f$ off $\{v,u\}$ (lamps at $v$ and $u$ unconstrained), and $0$ otherwise. Let $\pi_n(f,v) = 2^{-|\mathcal{V}_n|} \cdot \deg_{G_n}(v) / (2\,|E(G_n)|)$ (total division: identically $0$ if $G_n$ has no edges, as happens when $|\mathcal{V}_n| = 1$ ). Then $t_{\mathrm{mix}}(L_n) = \inf\{t \in \mathbb{N} : d_n(t) \le 1/4\}$ , where

d_n(t) = \sup_{s}\, \sup_{A} \Bigl|\sum_{s' \in A}(L_n^{\,t})(s,s') - \sum_{s' \in A}\pi_n(s')\Bigr|,

the sup running over starting states $s$ and subsets $A$ of the lamplighter state space; the $\mathbb{N}$ -infimum is $0$ if no such $t$ exists. ( $\pi_n$ is not hypothesized to be stationary for $L_n$ , nor $L_n$ to be stochastic — these are just the formulas above.)

Assertion. There exist real constants $c_1 > 0$ and $c_2 > 0$ and a natural number $N$ such that for all $n \ge N$ ,

c_1 \cdot t_{\mathrm{cov}}(Q_n) \;\le\; t_{\mathrm{mix}}(L_n) \quad\text{and}\quad t_{\mathrm{mix}}(L_n) \;\le\; c_2 \cdot t_{\mathrm{cov}}(Q_n),

with $t_{\mathrm{mix}}(L_n)$ cast from $\mathbb{N}$ to $\mathbb{R}$ and both inequalities non-strict. The constants $c_1, c_2, N$ are uniform in $n$ but may depend on the whole family $(G_n)$ .

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

tmix(G∗)≍tcov(G)t_{\mathrm{mix}}(G^\ast)\asymp t_{\mathrm{cov}}(G)tmix​(G∗)≍tcov​(G) for lamplighter chains

Read-back: lamplighter_mixing

$t_{\mathrm{mix}}(G^\ast)\asymp t_{\mathrm{cov}}(G)$ for lamplighter chains