Examples 1.12 and 1.20 -- simple random walk on a graph

Open

MarkovMixing.graph_walk_reversible

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

markov-chainsmixing-timesprobability

On a finite graph with no isolated vertices, simple random walk (move to a uniformly chosen neighbour) is a Markov chain; the distribution

\pi(x)=\frac{\deg(x)}{2|E|}

satisfies detailed balance with it, and is therefore its stationary distribution.

Preamble

import Definitions.Def_mm_basic

Formal statement

namespace MarkovMixing

/-- **Examples 1.12 and 1.20** (LPW): on a graph with no isolated vertices,
simple random walk is a Markov chain, the distribution
`π(x) = deg(x) / 2|E|` satisfies detailed balance, and it is stationary. -/
theorem graph_walk_reversible {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ x : V, 0 < G.degree x) :
    IsStochastic (graphWalk G) ∧
    DetailedBalance (graphWalk G)
      (fun x => (G.degree x : ℝ) / (2 * G.edgeFinset.card)) ∧
    IsStationary (graphWalk G)
      (fun x => (G.degree x : ℝ) / (2 * G.edgeFinset.card)) := 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, Sections 1.4-1.6, Examples 1.12 and 1.20, pp. 10 and 15

Read-back

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

Let $V$ be any finite, nonempty type with decidable equality, let $G$ be a simple graph on $V$ (undirected, no loops) with decidable adjacency, and assume every vertex has strictly positive degree: $\deg(x) > 0$ for all $x \in V$ . Define the real $V \times V$ matrix $P$ (the "graph walk" of $G$ ) entrywise by

P(x,y) = \begin{cases} \dfrac{1}{\deg(x)} & \text{if } x \sim y \text{ in } G, \\ 0 & \text{otherwise,} \end{cases}

and define the function $\pi : V \to \mathbb{R}$ by

\pi(x) = \frac{\deg(x)}{2\,|E|},

where $|E|$ is the number of edges of $G$ (the cardinality of its finite edge set; note that if $G$ had no edges this would be a division by zero, which in this formalization yields the value $0$ — though the positive-degree hypothesis rules that case out, since $V$ is nonempty). The theorem asserts the conjunction of the following three claims:

$P$ is stochastic: every entry satisfies $P(x,y) \ge 0$ , and every row sums to one, $\sum_{y \in V} P(x,y) = 1$ for all $x$ .
$P$ satisfies detailed balance with respect to $\pi$ : for all $x, y \in V$ ,

\pi(x)\,P(x,y) = \pi(y)\,P(y,x).

$\pi$ is a stationary distribution for $P$ , meaning both that $\pi$ is a probability distribution — $\pi(x) \ge 0$ for all $x$ and $\sum_{x \in V} \pi(x) = 1$ — and that $\pi$ is fixed by right multiplication as a row vector: $\pi P = \pi$ , i.e. $\sum_{x \in V} \pi(x)\,P(x,y) = \pi(y)$ for every $y \in V$ .

All three parts concern exactly this matrix $P$ and this function $\pi$ ; no irreducibility or aperiodicity is asserted, and no uniqueness of the stationary distribution is claimed.

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph