Propositions 2.12 and 2.14 -- random walks on finite groups

Open

MarkovMixing.group_walk_uniform_stationary

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

markov-chainsmixing-timesprobability

The random walk on a finite group $G$ with increment distribution $\mu$ (step from $a$ to $ha$ with probability $\mu(h)$ ) is a Markov chain for which the uniform distribution on $G$ is stationary; and if $\mu$ is symmetric ( $\mu(g^{-1})=\mu(g)$ ), the walk is reversible with respect to the uniform distribution.

Preamble

import Definitions.Def_mm_basic

Formal statement

namespace MarkovMixing

/-- **Propositions 2.12 and 2.14** (LPW): the random walk on a finite group
with increment distribution `μ` is a Markov chain for which the uniform
distribution is stationary; if `μ` is symmetric (`μ(g) = μ(g⁻¹)`), the walk is
moreover reversible. -/
theorem group_walk_uniform_stationary {G : Type*} [Group G] [Fintype G]
    [DecidableEq G] (μ : G → ℝ) (hμ : IsDist μ) :
    IsStochastic (groupWalk μ) ∧
    IsStationary (groupWalk μ) (uniformDist G) ∧
    ((∀ g : G, μ g⁻¹ = μ g) → DetailedBalance (groupWalk μ) (uniformDist G)) := 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 2.6, Propositions 2.12 and 2.14, pp. 28-29

Read-back

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

Let $G$ be a group that is also a finite type (with decidable equality), and let $\mu : G \to \mathbb{R}$ be a real-valued function on $G$ satisfying the hypothesis that $\mu$ is a distribution, meaning: $\mu(x) \ge 0$ for every $x \in G$ , and $\sum_{x \in G} \mu(x) = 1$ . Define the $G \times G$ real matrix $P$ (the "group walk" of $\mu$ ) entrywise by

P(a, b) = \mu(b \cdot a^{-1}) \quad \text{for all } a, b \in G,

and let $\pi : G \to \mathbb{R}$ be the constant function $\pi(x) = |G|^{-1}$ , where $|G|$ is the cardinality of $G$ (note that a group is necessarily nonempty, so $|G| \ge 1$ ). The theorem asserts the conjunction of three claims. (1) $P$ is stochastic: every entry satisfies $P(x,y) \ge 0$ , and every row sums to one, i.e. $\sum_{y \in G} P(x, y) = 1$ for each $x \in G$ . (2) $\pi$ is stationary for $P$ , which by the definition used here comprises two parts: $\pi$ is itself a distribution ( $\pi(x) \ge 0$ for all $x$ and $\sum_{x \in G} \pi(x) = 1$ ), and the row-vector–matrix product $\pi P$ equals $\pi$ , i.e.

\sum_{x \in G} \pi(x)\, P(x, y) = \pi(y) \quad \text{for every } y \in G.

(3) If additionally $\mu(g^{-1}) = \mu(g)$ for every $g \in G$ , then $P$ satisfies detailed balance with respect to $\pi$ , meaning

\pi(x)\, P(x, y) = \pi(y)\, P(y, x) \quad \text{for all } x, y \in G.

Only part (3) is conditional on the symmetry hypothesis $\mu(g^{-1}) = \mu(g)$ ; parts (1) and (2) are asserted for every distribution $\mu$ on $G$ . The group need not be abelian, and nothing beyond nonnegativity and total mass one is assumed of $\mu$ (in particular $\mu$ may vanish on generators or be concentrated at the identity, in which case $P$ is the corresponding — possibly reducible — transition matrix; the theorem asserts nothing about irreducibility, aperiodicity, or uniqueness of the stationary distribution).

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