Heat-kernel spectral bound $|H_t(x,y)-\pi(y)|\le\sqrt{\pi(y)/\pi(x)}\,e^{-\gamma t}$

Proved

MarkovMixing.heat_kernel_spectral_bound

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible Markov chain on a finite state space $V$ with stationary distribution $\pi$ , reversible with respect to it (detailed balance: $\pi(x)P(x,y)=\pi(y)P(y,x)$ ). The heat kernel at real time $t\ge0$ is $H_t(x,y)=\sum_ke^{-t}\tfrac{t^k}{k!}P^k(x,y)$ — the continuous-time chain driven by a rate-one Poisson clock. Among the eigenvalues of $P$ (real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$ ), $\lambda_2$ is the largest eigenvalue different from $1$ , and $\gamma=1-\lambda_2$ is the spectral gap (Mission VII).

The theorem (Theorem 20.6 of Levin–Peres–Wilmer) asserts the pointwise estimate: for all states $x,y$ and all $t\ge0$ ,

\bigl|H_t(x,y)-\pi(y)\bigr|\;\le\;\sqrt{\frac{\pi(y)}{\pi(x)}}\;e^{-\gamma t}.

In continuous time the convergence rate is governed by the spectral gap $\gamma$ itself — not the absolute gap $\gamma_\star$ of the discrete theory: negative eigenvalues, which cause the discrete chain to oscillate, are killed by the Poisson smoothing, since $P$ 's eigenvalue $\lambda$ becomes $e^{-(1-\lambda)t}$ for the heat kernel. The prefactor $\sqrt{\pi(y)/\pi(x)}$ comes from expanding the transition kernel in the $\ell^2(\pi)$ -orthonormal eigenbasis of Mission VII's spectral representation. This estimate is the continuous-time engine behind the product-chain theorem of this mission.

Preamble

import Definitions.Def_mm_continuous
import Mathlib.Analysis.SpecialFunctions.Sqrt

Formal statement

namespace MarkovMixing

/-- **Theorem 20.6** (LPW): for a reversible irreducible chain with spectral
gap `γ`, the heat kernel satisfies
`|H_t(x,y) − π(y)| ≤ √(π(y)/π(x)) e^{-γt}`. -/
theorem heat_kernel_spectral_bound {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (P : Matrix V V ℝ) (hP : IsStochastic P)
    (hirr : Irreducible P) (π : V → ℝ) (hπ : IsStationary P π)
    (hrev : DetailedBalance P π) (x y : V) (t : ℝ) (ht : 0 ≤ t) :
    |heatKernel P t x y - π y| ≤
      Real.sqrt (π y / π x) * Real.exp (-(spectralGap P) * 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 20.3, Theorem 20.6, Eq. (20.10), p. 268

Read-back

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

Read-back: heat_kernel_spectral_bound

Let $V$ be a finite, nonempty type with decidable equality, and let $P$ be a real $V \times V$ matrix that is stochastic (all entries $\ge 0$ ; each row sums, as a finite sum, to $1$ ) and irreducible (for all $x, y$ there is $t \in \mathbb{N}$ , possibly $0$ , with $(P^t)_{x,y} > 0$ ). Let $\pi : V \to \mathbb{R}$ be stationary for $P$ ( $\pi \ge 0$ pointwise, $\sum_x \pi(x) = 1$ , $\pi P = \pi$ as a row vector) and assume detailed balance: $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x, y$ . Then for every pair of states $x, y \in V$ and every real $t$ with $t \ge 0$ , the theorem asserts the pointwise bound

\big| H_t(x,y) - \pi(y) \big| \;\le\; \sqrt{\frac{\pi(y)}{\pi(x)}} \;\cdot\; e^{-\gamma\, t},

where $H_t(x,y) = \sum'_{k \ge 0} \frac{e^{-t} t^k}{k!} (P^k)_{x,y}$ is the heat-kernel entry (a tsum over $k$ , taking the junk value $0$ if the family is not summable), and $\gamma$ is the spectral gap defined as

\gamma = 1 - \sup\{\, \lambda \in \mathbb{R} \mid \exists f : V \to \mathbb{R},\ f \ne 0,\ P f = \lambda f,\ \lambda \ne 1 \,\},

i.e. one minus the real supremum of the set of real numbers $\lambda \ne 1$ that admit a nonzero real (right-)eigenvector of $P$ (eigenvectors of $P$ acting on column vectors; complex or defective spectrum is not seen by this definition). Junk-value behavior that the bound's meaning may depend on: the real supremum defining $\gamma$ is $0$ when the eigenvalue set is empty (giving $\gamma = 1$ ); the quotient $\pi(y)/\pi(x)$ is real division, so if $\pi(x) = 0$ it takes the junk value $0$ and the right-hand side collapses to $0 \cdot e^{-\gamma t} = 0$ , making the claim at such $x$ an exact equality requirement $H_t(x,y) = \pi(y)$ ; and $\sqrt{\cdot}$ is the real square root, which returns $0$ on negative inputs (not relevant here since $\pi \ge 0$ , but part of the function used). The bound is asserted entrywise for each $(x,y)$ separately, with the same exponential rate $\gamma$ for all entries.

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

Heat-kernel spectral bound ∣Ht(x,y)−π(y)∣≤π(y)/π(x) e−γt|H_t(x,y)-\pi(y)|\le\sqrt{\pi(y)/\pi(x)}\,e^{-\gamma t}∣Ht​(x,y)−π(y)∣≤π(y)/π(x)​e−γt

Read-back: heat_kernel_spectral_bound

Heat-kernel spectral bound $|H_t(x,y)-\pi(y)|\le\sqrt{\pi(y)/\pi(x)}\,e^{-\gamma t}$