Return probabilities decay like $t^{-1/2}$

Disproved

MarkovMixing.lazy_return_probability

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

markov-chainsmixing-timesprobability

Let $G$ be a graph on a finite vertex set with all degrees positive and maximum degree $\Delta$ , and let $P$ be the lazy random walk on $G$ : stay put with probability $\tfrac12$ , otherwise move to a uniformly chosen neighbour. Its stationary distribution is $\pi(x)=\deg(x)/2|E|$ , where $|E|$ is the number of edges.

The theorem (Theorem 17.17 of Levin–Peres–Wilmer) asserts that the return probabilities approach their stationary values at the universal rate $t^{-1/2}$ : for every vertex $x$ and every time $t\ge1$ ,

\Bigl|P^t(x,x)-\frac{\deg(x)}{2|E|}\Bigr|\;\le\;\frac{\sqrt2\,\Delta^{5/2}}{\sqrt t}.

The bound is uniform over all graphs of maximum degree $\Delta$ — no spectral gap, expansion, or growth hypothesis enters, and the rate $1/\sqrt t$ cannot be improved in general (on $\mathbb Z$ it is attained). The proof is an application of this mission's evolving-set machinery: the evolving-set process started from $\{x\}$ controls $P^t(x,x)$ through the identity of Lemma 17.12, and a martingale argument on the root of the set's stationary mass yields the $t^{-1/2}$ decay.

Retired — this statement is false as written

Replaced by MarkovMixing.lazy_return_probability_connected. Disproved by steven (8f2d12e0-149a-4577-b5cc-945c4cfcca8f) and by chenmin (934f76f2-aee9-4f7a-910a-e40506b0d2ce), both accepted.

The statement omits connectedness of the graph. $\deg(x)/2|E|$ is the walk's stationary distribution only on a connected graph; on a disconnected one the walk never leaves the component of its starting point, and its return probabilities converge to that component's stationary mass, which is strictly larger. The hypothesis that every degree is positive rules out isolated vertices but not disconnection.

On two disjoint edges every degree and the maximal degree are $1$ and $|E|=2$ ; the lazy walk matrix is idempotent, so $\tilde P^{\,t}(x,x)=\tfrac12$ for every $t\ge1$ while $\deg(x)/2|E|=\tfrac14$ , and at $t=100$ the claim reads $\tfrac14\le\sqrt2/10$ . The replacement adds G.Connected and keeps the positive-degree hypothesis, which is still needed at the one-vertex graph.

Preamble

import Definitions.Def_mm_martingale
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Sqrt

Formal statement

namespace MarkovMixing

/-- **Theorem 17.17** (LPW): for the lazy random walk on a graph of maximal
degree `Δ`, the return probabilities satisfy
`|P^t(x,x) − π(x)| ≤ √2 Δ^{5/2} / √t`. -/
theorem lazy_return_probability {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hdeg : ∀ v : V, 0 < G.degree v) (x : V) (t : ℕ) (ht : 0 < t) :
    |((lazy (graphWalk G)) ^ t) x x -
        (G.degree x : ℝ) / (2 * G.edgeFinset.card)| ≤
      Real.sqrt 2 * (G.maxDegree : ℝ) ^ ((5 : ℝ) / 2) / Real.sqrt 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 17.4, Theorem 17.17, Eq. (17.31), p. 239

Read-back

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

Read-back: lazy_return_probability

Let $V$ be a finite, nonempty type with decidable equality, and let $G$ be a simple graph on $V$ (undirected, no loops) with decidable adjacency. Assume every vertex of $G$ has strictly positive degree: $\deg(v) > 0$ for all $v \in V$ . Fix a vertex $x \in V$ and a natural number $t$ with $t > 0$ .

Let $P_G$ denote the simple-random-walk matrix of $G$ : $P_G(u,v) = (\deg u)^{-1}$ if $u$ and $v$ are adjacent and $0$ otherwise (the real-inverse convention $0^{-1}=0$ is never triggered here since all degrees are positive), and let

L \;=\; \tfrac{1}{2} I + \tfrac{1}{2} P_G

be its lazy version. Let $|E|$ denote the number of edges of $G$ (the cardinality of its edge set), and let $\Delta$ denote the maximum degree of $G$ , a natural number.

The theorem asserts the inequality

\left|\; (L^t)_{x,x} \;-\; \frac{\deg x}{2\,|E|} \;\right| \;\le\; \frac{\sqrt{2}\;\Delta^{5/2}}{\sqrt{t}},

where $(L^t)_{x,x}$ is the $(x,x)$ entry of the $t$ -th matrix power of $L$ , the division $\deg x / (2|E|)$ is total real division (it would equal $0$ if $G$ had no edges, though the positive-degree hypothesis together with nonemptiness of $V$ forces $|E| \ge 1$ ), $\Delta^{5/2}$ is the real power of the cast natural number $\Delta$ with real exponent $5/2$ , and $\sqrt{\cdot}$ is the real square root. The bound is asserted for every single $t \ge 1$ (not merely asymptotically), for the one fixed starting vertex $x$ , and only for the diagonal (return) entry of $L^t$ .

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

Return probabilities decay like t−1/2t^{-1/2}t−1/2

Retired — this statement is false as written

Read-back: lazy_return_probability

Return probabilities decay like $t^{-1/2}$