Edge removal perturbs the spectral gap by at most $e^{2\beta(\Delta+2r)}$

Proved

MarkovMixing.ising_edge_removal

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

markov-chainsmixing-timesprobability

Let $G$ be a graph with maximum degree $\Delta$ on a finite vertex set, and let $G'\subseteq G$ be a subgraph obtained by deleting $r$ edges (all vertices kept). For a graph $H$ , the Ising model at inverse temperature $\beta>0$ is the distribution $\pi_H(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}\in E(H)}\sigma(v)\sigma(w)\bigr)$ on spin configurations $\sigma:V\to\{\pm1\}$ , and its Glauber dynamics re-samples a uniformly chosen site from the conditional distribution. The spectral gap of a chain is $\gamma=1-\lambda_2$ , where $\lambda_2$ is the largest eigenvalue different from $1$ (an eigenvalue being a real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$ , as in Mission VII).

The theorem (Proposition 15.7 of Levin–Peres–Wilmer) asserts that deleting the $r$ edges changes the spectral gap by at most an explicit exponential factor:

\gamma_{G'}\;\le\;e^{\,2\beta(\Delta+2r)}\;\gamma_{G},

where $\gamma_H$ denotes the gap of the Glauber dynamics for the Ising model on $H$ .

The proof is a direct comparison of Dirichlet forms (Mission VII): removing $r$ edges changes every Gibbs weight by at most $e^{2\beta r}$ and every transition probability by at most $e^{2\beta\Delta}$ . In the book this is the key surgery step for the tree bound: cutting the root's edges splits the tree into independent subtrees, at a bounded cost in the gap.

Preamble

import Definitions.Def_mm_ising

Formal statement

namespace MarkovMixing

/-- **Proposition 15.7** (LPW): removing `r` edges from a graph of maximal
degree `Δ` changes the spectral gap of the Ising Glauber dynamics by at most
a factor `e^{2β(Δ + 2r)}`:  `γ̃ ≤ e^{2β(Δ+2r)} γ` is equivalent to the
stated `1/γ ≤ e^{2β(Δ+2r)}/γ̃`. -/
theorem ising_edge_removal {Vv : Type*} [Fintype Vv] [DecidableEq Vv]
    [Nonempty Vv] (G G' : SimpleGraph Vv) [DecidableRel G.Adj]
    [DecidableRel G'.Adj] (hsub : G' ≤ G) (β : ℝ) (hβ : 0 < β) :
    spectralGap (glauber (isingDist G' β)) ≤
      Real.exp (2 * β * ((G.maxDegree : ℝ) +
        2 * ((G.edgeFinset \ G'.edgeFinset).card : ℝ))) *
      spectralGap (glauber (isingDist G β)) := 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 15.4, Proposition 15.7, p. 207

Read-back

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

Read-back: ising_edge_removal

Setting. Let $V$ be a finite, nonempty type with decidable equality, and let $G, G'$ be two simple graphs on $V$ (each with decidable adjacency) satisfying $G' \le G$ , i.e. every edge of $G'$ is an edge of $G$ . Let $\beta$ be a real with $\beta > 0$ .

Unfolding the custom notions: for a graph $H$ , $\mu_H$ denotes the Ising measure on configurations $\sigma : V \to \{\pm1\}$ , $\mu_H(\sigma) = w_H(\sigma)/\sum_\tau w_H(\tau)$ with $w_H(\sigma) = \exp\big(\beta \sum_{\{v,w\} \in E(H)} s_\sigma(v)s_\sigma(w)\big)$ (the code's ordered double sum with a factor $\tfrac12$ ). $\mathrm{glauber}(\mu_H)$ is the single-site heat-bath chain: from $\sigma$ , pick a uniform vertex $v$ (probability $1/|V|$ each) and resample the spin at $v$ from $\mu_H$ conditioned on the other spins. For any matrix $P$ on configurations, the spectral gap as defined here is

\gamma(P) \;=\; 1 - \sup\{\lambda \in \mathbb{R} \;:\; \exists f \ne 0,\ P f = \lambda f,\ \lambda \ne 1\},

where the supremum is the real sSup, which takes the junk value $0$ if the set of such eigenvalues is empty or unbounded above — in that case $\gamma(P) = 1$ . Note this $\lambda_2$ is the supremum of all real eigenvalues other than exactly $1$ (negative eigenvalues and eigenvalues $> 1$ included; only the value $1$ itself is excluded), with no reversibility or symmetry assumed in the definition.

The claim. Under these hypotheses,

\gamma\big(\mathrm{glauber}(\mu_{G'})\big) \;\le\; \exp\!\Big( 2\beta\big(\Delta_G + 2\,|E(G)\setminus E(G')|\big)\Big)\cdot \gamma\big(\mathrm{glauber}(\mu_{G})\big),

where $\Delta_G$ is the maximum degree of the larger graph $G$ (a natural number cast to $\mathbb{R}$ ) and $|E(G)\setminus E(G')|$ is the number of edges of $G$ that are not edges of $G'$ (cardinality of the edge-finset difference, cast to $\mathbb{R}$ ).

Direction of the inequality: it is the gap of the chain on the subgraph $G'$ that is bounded above by $e^{2\beta(\Delta_G + 2|E(G)\setminus E(G')|)}$ times the gap of the chain on $G$ . The exponential factor uses $\Delta_G$ (not $\Delta_{G'}$ ) and counts each removed edge with weight $2$ . No hypothesis is placed on connectivity, on the number of removed edges, or on the sign of either spectral gap (the sSup-based gaps could a priori be negative or take the junk value described above); $G' = G$ is allowed, in which case the factor is $e^{2\beta\Delta_G} \ge 1$ .

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

Edge removal perturbs the spectral gap by at most e2β(Δ+2r)e^{2\beta(\Delta+2r)}e2β(Δ+2r)

Read-back: ising_edge_removal

Edge removal perturbs the spectral gap by at most $e^{2\beta(\Delta+2r)}$