Lazy vs continuous-time mixing

Proved

MarkovMixing.continuous_discrete_mixing

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$ . Two slowed-down versions of $P$ are compared: the lazy chain $\tilde P=\tfrac12(I+P)$ , which holds with probability $\tfrac12$ each step, and the continuous-time chain, whose distribution at real time $t$ is the heat kernel

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

— $P$ -jumps taken at the arrivals of a rate-one Poisson clock. Distances are total variation, $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ .

The theorem (Theorem 20.3 of Levin–Peres–Wilmer) asserts that the two regularizations mix at comparable times, for every $\varepsilon>0$ :

for all sufficiently large $k$ : if the lazy chain is within $\varepsilon$ of $\pi$ at time $k$ from a state $x$ , then the continuous chain is within $2\varepsilon$ at the same time $k$ ;
for all sufficiently large $m$ : if the continuous chain is within $\varepsilon$ of $\pi$ at time $m$ from $x$ , then the lazy chain is within $2\varepsilon$ at time $4m$ .

Nothing about mixing is lost (beyond constant factors) in passing between the lazy and the Poissonized regularization. The proof matches the two random clocks: the number of $P$ -steps completed by the lazy chain in $4m$ steps is Binomial $(4m,\tfrac12)$ , which merges in total variation with (a shifted) Poisson $(m)$ — so the two chains can be driven by nearly the same number of genuine jumps.

Retired — this statement is true but empty

Replaced by MarkovMixing.continuous_discrete_mixing_uniform. Proved by chenmin (accepted), who reported in the same submission that the statement has no content; this note follows that analysis. The proof stands and is unaffected by the retirement.

Both halves have the shape $\exists K,\ \forall k\ge K,\ (\Phi(k,x)<\varepsilon\Rightarrow\Psi(k,x)<2\varepsilon)$ with $K$ quantified after the chain. For a fixed finite irreducible chain both $d^{\mathrm{cont}}(t)$ and the lazy chain's distance to $\pi$ tend to $0$ , so any large enough $K$ makes each conclusion hold outright and the antecedent is never read. The statement is therefore subsumed by Theorem 20.1 (heat_kernel_convergence), and the constants $4$ and $2\varepsilon$ could be replaced by anything — by $1$ and $\varepsilon/1000$ — without affecting provability. Nothing of the Binomial–Poisson clock comparison, which is the actual content of LPW Theorem 20.3, is expressible in it.

The replacement quantifies both thresholds before the chain, uniformly over all finite irreducible chains. That is what LPW's proof delivers, and under it the shortcut dies: mixing times are unbounded across the family, so no single threshold can be read off any one chain.

Preamble

import Definitions.Def_mm_continuous

Formal statement

namespace MarkovMixing

/-- **Theorem 20.3** (LPW): comparison of continuous-time and lazy
discrete-time mixing.  (i) For sufficiently large `k`, if the lazy chain is
`ε`-mixed at time `k`, the heat kernel is `2ε`-mixed at time `k`.  (ii) For
sufficiently large `m`, if the heat kernel is `ε`-mixed at time `m`, the
lazy chain is `2ε`-mixed at time `4m`. -/
theorem continuous_discrete_mixing {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (P : Matrix V V ℝ) (hP : IsStochastic P)
    (hirr : Irreducible P) (π : V → ℝ) (hπ : IsStationary P π)
    (ε : ℝ) (hε : 0 < ε) :
    (∃ K : ℕ, ∀ k : ℕ, K ≤ k → ∀ x : V,
      tvDist (rowDist (lazy P) k x) π < ε →
        tvDist (fun y => heatKernel P k x y) π < 2 * ε) ∧
    (∃ M : ℕ, ∀ m : ℕ, M ≤ m → ∀ x : V,
      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.3, Theorem 20.3, p. 266

Read-back

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

Read-back: continuous_discrete_mixing

Let $V$ be a finite, nonempty type with decidable equality, $P$ 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$ ), and $\pi : V \to \mathbb{R}$ stationary for $P$ (meaning $\pi \ge 0$ pointwise, $\sum_x \pi(x) = 1$ , and the row-vector identity $\pi P = \pi$ ). Let $\varepsilon$ be a real number with $\varepsilon > 0$ . Write $d_{TV}(\mu,\nu) = \sup_{A \subseteq V} \big|\sum_{x\in A}\mu(x) - \sum_{x \in A}\nu(x)\big|$ (supremum over all finite subsets $A$ of $V$ , the empty set included), write $L = \tfrac12 I + \tfrac12 P$ for the lazy chain, and write

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

for the heat kernel at real time $s$ (a tsum over $k$ , taking the junk value $0$ on any entry where the family is not summable). The theorem asserts the conjunction of two claims:

There exists a natural number $K$ such that for every natural $k \ge K$ and every state $x$ : if $d_{TV}\big((L^k)_{x,\cdot},\, \pi\big) < \varepsilon$ (row $x$ of the $k$ -th power of the lazy chain), then $d_{TV}\big(H_k(x,\cdot),\, \pi\big) < 2\varepsilon$ , where the heat kernel is evaluated at the real cast of the same $k$ .
There exists a natural number $M$ such that for every natural $m \ge M$ and every state $x$ : if $d_{TV}\big(H_m(x,\cdot),\, \pi\big) < \varepsilon$ , then $d_{TV}\big((L^{4m})_{x,\cdot},\, \pi\big) < 2\varepsilon$ , i.e. the lazy chain run for $4m$ discrete steps.

Both inner statements are implications (strict $<$ on both sides, with threshold $2\varepsilon$ in the conclusions): they only constrain what happens when the respective premise distance is below $\varepsilon$ , and hold vacuously at any $(k, x)$ or $(m, x)$ where the premise fails. The existential thresholds $K$ and $M$ may depend on all the ambient data but not on $x$ .

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