Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 20.3 -- lazy chain versus continuous time, uniformly in the chain

Proved
MarkovMixing.continuous_discrete_mixing_uniform

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

markov-chainsmixing-timesprobability

Let PPP be the transition matrix of a finite irreducible Markov chain (from any state, any other is reachable in some number of steps), with stationary distribution π\piπ; the chain need not be aperiodic or reversible. Two derived chains are compared. The lazy chain P~=12(I+P)\tilde P=\tfrac12(I+P)P~=21​(I+P) flips a fair coin at each step and moves according to PPP only on heads. The continuous-time chain runs PPP at the jump times of a rate-one Poisson process; its transition kernel is the heat kernel

Ht(x,y)=∑k≥0e−ttkk! Pk(x,y),H_t(x,y)=\sum_{k\ge0}e^{-t}\frac{t^k}{k!}\,P^k(x,y),Ht​(x,y)=k≥0∑​e−tk!tk​Pk(x,y),

the law of the chain after a Poisson(t)(t)(t) number of steps. Distances to equilibrium are measured in total variation, ∥μ−ν∥TV=max⁡A∣μ(A)−ν(A)∣\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|∥μ−ν∥TV​=maxA​∣μ(A)−ν(A)∣.

The theorem (Theorem 20.3 of Levin–Peres–Wilmer) asserts that the two clocks agree up to a bounded factor, with thresholds that depend on the accuracy alone and not on the chain. Fix ε>0\varepsilon>0ε>0. Then:

  1. there is a KKK such that for every finite irreducible chain, every k≥Kk\ge Kk≥K and every state xxx: ∥P~ k(x,⋅)−π∥TV<ε\|\tilde P^{\,k}(x,\cdot)-\pi\|_{TV}<\varepsilon∥P~k(x,⋅)−π∥TV​<ε implies ∥Hk(x,⋅)−π∥TV<2ε\|H_k(x,\cdot)-\pi\|_{TV}<2\varepsilon∥Hk​(x,⋅)−π∥TV​<2ε;
  2. there is an MMM such that for every finite irreducible chain, every m≥Mm\ge Mm≥M and every state xxx: ∥Hm(x,⋅)−π∥TV<ε\|H_m(x,\cdot)-\pi\|_{TV}<\varepsilon∥Hm​(x,⋅)−π∥TV​<ε implies ∥P~ 4m(x,⋅)−π∥TV<2ε\|\tilde P^{\,4m}(x,\cdot)-\pi\|_{TV}<2\varepsilon∥P~4m(x,⋅)−π∥TV​<2ε.

This is the bridge between the discrete and continuous theories, and the reason a mixing bound proved on one side transfers to the other with only a constant factor lost. Part (2) is the harder half: it rests on Lemma 20.4, the statement that a binomial (4m,12)(4m,\tfrac12)(4m,21​) variable and m+m+{}m+Poisson(m)(m)(m) merge in total variation as m→∞m\to\inftym→∞ — the two clocks can be coupled, since both have mean 2m2m2m and variance mmm.

A note on the order of the quantifiers. The thresholds are quantified before the chain. LPW say "for sufficiently large kkk", and their proof delivers exactly that reading: the error in (2) is the total variation distance between the two clock distributions, a quantity that does not see the chain at all, and the estimate behind (1) is P{N2k<k}→0\mathbb P\{N_{2k}<k\}\to0P{N2k​<k}→0 for a Poisson process. If instead the threshold may be chosen after the chain, the statement says nothing: for a fixed finite irreducible chain both ∥Ht(x,⋅)−π∥TV\|H_t(x,\cdot)-\pi\|_{TV}∥Ht​(x,⋅)−π∥TV​ and ∥P~ t(x,⋅)−π∥TV\|\tilde P^{\,t}(x,\cdot)-\pi\|_{TV}∥P~t(x,⋅)−π∥TV​ tend to 000, so any sufficiently large threshold makes each conclusion true outright and the hypothesis of the implication is never used — the two halves then reduce to the convergence theorem, and the constants 444 and 2ε2\varepsilon2ε could be replaced by anything. Quantified as above the shortcut disappears, because mixing times are unbounded across the family of finite chains and no single threshold can be read off any one of them. Chains are taken on the state spaces {0,1,…,n−1}\{0,1,\dots,n-1\}{0,1,…,n−1}, which costs nothing since every finite state space is in bijection with one.

Preamble
import Definitions.Def_mm_continuous
Formal statement
namespace MarkovMixing

/-- **Theorem 20.3** (LPW): the discrete lazy chain and the continuous-time
chain mix at comparable times.  For every `ε > 0` there is a threshold `K`,
*depending on `ε` alone*, such that for every finite irreducible chain: for
`k ≥ K`, `‖P̃^k(x,·) − π‖ < ε` implies `‖H_k(x,·) − π‖ < 2ε`; and there is a
threshold `M`, again depending on `ε` alone, such that for `m ≥ M`,
`‖H_m(x,·) − π‖ < ε` implies `‖P̃^{4m}(x,·) − π‖ < 2ε`.

The thresholds are quantified before the chain.  LPW say "for sufficiently
large `k`", and their proof produces a bound that does not see the chain at
all: part (ii) rests on Lemma 20.4, the statement that binomial `(4m,1/2)`
and `m +` Poisson `(m)` merge in total variation, a fact about the two clocks
and nothing else; part (i) rests on `P{N_{2k} < k} → 0` for `N` Poisson.  If
instead the threshold may be chosen after the chain, the statement collapses:
both `d^cont(t)` and the distance of the lazy chain tend to `0` for a fixed
irreducible chain, so any large enough threshold makes the conclusion hold
outright and the hypothesis is never read.  Quantified as here, no single
threshold can be read off one chain, because mixing times are unbounded over
the family, and the Binomial--Poisson comparison is forced.

Chains are taken on `Fin n`, which is no loss: every finite state space is in
bijection with one, and the thresholds are what the statement is about. -/
theorem continuous_discrete_mixing_uniform (ε : ℝ) (hε : 0 < ε) :
    (∃ K : ℕ, ∀ (n : ℕ) (P : Matrix (Fin n) (Fin n) ℝ), IsStochastic P →
      Irreducible P → ∀ π : Fin n → ℝ, IsStationary P π →
      ∀ k : ℕ, K ≤ k → ∀ x : Fin n,
        tvDist (rowDist (lazy P) k x) π < ε →
          tvDist (fun y => heatKernel P k x y) π < 2 * ε) ∧
    (∃ M : ℕ, ∀ (n : ℕ) (P : Matrix (Fin n) (Fin n) ℝ), IsStochastic P →
      Irreducible P → ∀ π : Fin n → ℝ, IsStationary P π →
      ∀ m : ℕ, M ≤ m → ∀ x : Fin n,
        tvDist (fun y => heatKernel P m x y) π < ε →
          tvDist (rowDist (lazy P) (4 * m) x) π < 2 * ε) := 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.3, p. 266

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me