$t_{\mathrm{rel}}(G^\ast)\asymp t_{\mathrm{hit}}(G)$ for lamplighter chains

Proved

MarkovMixing.lamplighter_relaxation

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$ . Over each $G_n$ two chains are compared. The base walk is the lazy simple random walk on $G_n$ (hold with probability $\tfrac12$ , else move to a uniform neighbour), with maximal hitting time $t_{\mathrm{hit}}(G_n)=\max_{x,y}\mathbb E_x(\tau_y)$ , the worst expected time to reach one vertex from another (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 step of the base walk, and randomizes the lamp at the new position. Among the eigenvalues of a chain (real $\lambda$ with $Pf=\lambda f$ , $f\ne0$ ), $\lambda_\star$ is the largest absolute value of an eigenvalue $\ne1$ , and the relaxation time is $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ (Mission VII).

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

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

The lamplighter's slowest mode is governed by the base walk's worst hitting time: to decorrelate, the lamplighter must revisit far-away lamps. The lower bound tests the variational characterization of the gap (Mission VII) with an eigenfunction built from an unvisited-vertex indicator; the upper bound is a coupling-contraction estimate. Together with the companion theorem ( $t_{\mathrm{mix}}\asymp t_{\mathrm{cov}}$ ), the lamplighter ties the hitting, cover, relaxation, and mixing parameters of the whole series into one family.

Preamble

import Definitions.Def_mm_cutoff

Formal statement

namespace MarkovMixing

/-- **Theorem 19.1** (LPW): the relaxation time of the lamplighter chain is
comparable to the maximal hitting time of the underlying lazy walk: there
are constants `c₁, c₂ > 0` such that for all sufficiently large `n`,
`c₁ t_hit(G_n) ≤ t_rel(G_n⁎) ≤ c₂ t_hit(G_n)`. -/
theorem lamplighter_relaxation {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₁ * hitTimeMax (lazy (graphWalk (G n))) ≤
        relaxationTime (lamplighter (G n)) ∧
      relaxationTime (lamplighter (G n)) ≤
        c₂ * hitTimeMax (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.2, Theorem 19.1, Eq. (19.2), p. 258

Read-back

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

Read-back: lamplighter_relaxation

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 link between the index $n$ and the graph is assumed). Let $Q_n = \tfrac12 I + \tfrac12 W_n$ be the lazy simple random walk on $G_n$ , with $W_n(x,y) = (\deg_{G_n} x)^{-1}$ for $x \sim y$ and $0$ otherwise ( $0^{-1}=0$ on isolated vertices). Define two quantities.

Maximal hitting time. $t_{\mathrm{hit}}(Q_n) = \sup_{(x,y)} \sum_{t=0}^{\infty} a_{x,y}(t)$ , the supremum over all ordered pairs $(x,y)$ of vertices of the infinite sum over $t \in \mathbb{N}$ of $a_{x,y}(t)$ , where $a_{x,y}(t)$ is the sum, over all trajectories $\omega = (\omega_0,\dots,\omega_t)$ with $\omega_0 = x$ and $\omega_i \ne y$ for every $i \le t$ (including $i = 0$ ), of $\prod_{i<t} Q_n(\omega_i,\omega_{i+1})$ — the probability that the walk started at $x$ has avoided $y$ through time $t$ . Note that for the diagonal pairs $x = y$ the condition fails at $i=0$ , so those pairs contribute $0$ to the supremum. The sum over $t$ is Lean's tsum, equal to the junk value $0$ if the family is not summable; the supremum is a real supremum over the finite nonempty set of pairs.

Relaxation time of the lamplighter chain. Let $L_n$ be the lamplighter matrix on states $(f,v)$ , $f : \mathcal{V}_n \to \{\text{off},\text{on}\}$ , $v \in \mathcal{V}_n$ : transition probability from $(f,v)$ to $(g,u)$ equal to $Q_n(v,v)/2 = 1/4$ if $u = v$ and $g = f$ off $v$ (lamp at $v$ unconstrained); $Q_n(v,u)/4$ if $u \ne v$ and $g = f$ off $\{v,u\}$ (lamps at $v$ and $u$ unconstrained); $0$ otherwise. Its relaxation time is

t_{\mathrm{rel}}(L_n) \;=\; \bigl(1 - \lambda^\star(L_n)\bigr)^{-1}, \qquad \lambda^\star(L_n) = \sup\bigl\{|\lambda| : \lambda \in \mathbb{R},\ \lambda \ne 1,\ \exists f \ne 0,\ L_n f = \lambda f\bigr\},

where the eigenvalue condition means there is a nonzero real vector $f$ on the lamplighter state space with the matrix acting on column vectors satisfying $L_n f = \lambda f$ . Junk conventions: the real supremum of an empty set is $0$ ; the inverse is total, so if $\lambda^\star(L_n) = 1$ then $t_{\mathrm{rel}}(L_n) = 0^{-1} = 0$ . Only real eigenvalues enter; $\lambda = 1$ is excluded but values $> 1$ or $\le -1$ , if any, are not.

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

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

both inequalities non-strict, with $c_1, c_2, N$ uniform over $n \ge N$ . Nothing is asserted or assumed about stochasticity of $L_n$ or about any stationary distribution — the two sides are exactly the formulas above.

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

trel(G∗)≍thit(G)t_{\mathrm{rel}}(G^\ast)\asymp t_{\mathrm{hit}}(G)trel​(G∗)≍thit​(G) for lamplighter chains

Read-back: lamplighter_relaxation

$t_{\mathrm{rel}}(G^\ast)\asymp t_{\mathrm{hit}}(G)$ for lamplighter chains