Continuous-time convergence without aperiodicity

Proved

MarkovMixing.heat_kernel_convergence

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$ — aperiodicity is not assumed — with stationary distribution $\pi$ . The heat kernel at real time $t$ is

H_t(x,y)=\sum_{k=0}^{\infty}e^{-t}\frac{t^k}{k!}\,P^k(x,y),

the law at time $t$ of the walk taking $P$ -steps at the arrival times of a rate-one Poisson clock. Write $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance and $d^{\mathrm{cont}}(t)=\max_x\|H_t(x,\cdot)-\pi\|_{TV}$ .

The theorem (Theorem 20.1 of Levin–Peres–Wilmer) asserts:

d^{\mathrm{cont}}(t)\;\longrightarrow\;0\qquad(t\to\infty).

Every irreducible finite chain converges in continuous time — the periodicity obstruction that forces the aperiodicity hypothesis in the discrete Convergence Theorem (Mission II) simply disappears, because the Poisson number of completed jumps spreads over all residue classes: $H_t(x,x)>0$ for every $t>0$ , so the continuous chain is automatically "aperiodic". This is the basic payoff of the continuous-time formalism and the reason laziness can always be traded for Poissonization.

Preamble

import Definitions.Def_mm_continuous

Formal statement

namespace MarkovMixing

/-- **Theorem 20.1** (LPW): for an irreducible chain — aperiodicity is *not*
needed — the heat kernel converges to the stationary distribution:
`max_x ‖H_t(x,·) − π‖_TV → 0` as `t → ∞`. -/
theorem heat_kernel_convergence {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (P : Matrix V V ℝ) (hP : IsStochastic P)
    (hirr : Irreducible P) (π : V → ℝ) (hπ : IsStationary P π) :
    Filter.Tendsto (fun t : ℝ => contDistStationary P π t)
      Filter.atTop (nhds 0) := 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.2, Theorem 20.1, p. 266

Read-back

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

Read-back: heat_kernel_convergence

Let $V$ be a finite, nonempty type with decidable equality, $P$ a real $V \times V$ matrix that is stochastic (all entries $\ge 0$ and each row sums, as a finite sum, to $1$ ) and irreducible (for all $x, y$ there exists $t \in \mathbb{N}$ , possibly $0$ , with $(P^t)_{x,y} > 0$ ), and $\pi : V \to \mathbb{R}$ stationary for $P$ (i.e. $\pi \ge 0$ pointwise, $\sum_x \pi(x) = 1$ , and $\pi P = \pi$ as a row vector). The conclusion asserts that the function

t \;\longmapsto\; \sup_{x \in V} \, d_{TV}\big(H_t(x,\cdot),\, \pi\big)

tends to $0$ as the real time parameter $t \to +\infty$ (limit along the real at-top filter, so $t$ ranges over all reals, not just naturals). Here $H_t$ is the heat kernel

H_t(x,y) = \sum_{k=0}^{\infty}{}' \frac{e^{-t}\, t^k}{k!}\, (P^k)_{x,y},

a tsum over $k \in \mathbb{N}$ whose value is the junk value $0$ on any entry where the family in $k$ fails to be summable, and

d_{TV}(\mu, \nu) = \sup_{A \subseteq V} \Big|\sum_{x \in A}\mu(x) - \sum_{x \in A}\nu(x)\Big|

is the supremum over all (finite) subsets $A$ of $V$ , including $A = \varnothing$ , of the absolute difference of masses; the outer supremum over $x$ is over the nonempty finite type $V$ . No aperiodicity hypothesis appears (none is needed to state the claim), no rate of convergence is asserted, and no uniqueness or further property of $\pi$ is claimed — only that this particular worst-case-over-starting-state distance converges to $0$ in continuous time.

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