Lemma 12.2 -- the spectral representation of a reversible chain

Proved

MarkovMixing.spectral_representation

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ with $n=|V|$ states, reversible with respect to a strictly positive probability distribution $\pi$ — that is, satisfying the detailed balance equations $\pi(x)P(x,y)=\pi(y)P(y,x)$ . Equip real-valued functions on $V$ with the weighted inner product

\langle f,g\rangle_\pi=\sum_{x\in V}f(x)\,g(x)\,\pi(x),

the geometry in which a reversible chain is self-adjoint.

The theorem (Lemma 12.2 of Levin–Peres–Wilmer) asserts the existence of real numbers $\lambda_1,\dots,\lambda_n$ and functions $f_1,\dots,f_n:V\to\mathbb R$ such that:

each $f_j$ is an eigenfunction, $Pf_j=\lambda_jf_j$ (with $(Pf)(x)=\sum_yP(x,y)f(y)$ );
the family is orthonormal in $\ell^2(\pi)$ : $\langle f_j,f_k\rangle_\pi=1$ if $j=k$ and $0$ otherwise;
the transition probabilities decompose spectrally: for every time $t$ and all states $x,y$ ,

\frac{P^t(x,y)}{\pi(y)}=\sum_{j=1}^{n}f_j(x)\,f_j(y)\,\lambda_j^{\,t}.

Every question about the long-run behaviour of a reversible chain thereby becomes a question about the decay of the powers $\lambda_j^t$ — the formula from which the relaxation-time bounds of this mission and the cutoff theory of later missions are read off.

Preamble

import Definitions.Def_mm_spectral

Formal statement

namespace MarkovMixing

/-- **Lemma 12.2** (LPW): a chain reversible with respect to a positive
distribution `π` admits an orthonormal basis of `ℓ²(π)` consisting of real
eigenfunctions, and the transition probabilities decompose spectrally:
`P^t(x,y)/π(y) = ∑_j f_j(x) f_j(y) λ_j^t`. -/
theorem spectral_representation {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsDist π) (hpos : ∀ x : V, 0 < π x)
    (hrev : DetailedBalance P π) :
    ∃ (lam : Fin (Fintype.card V) → ℝ) (f : Fin (Fintype.card V) → V → ℝ),
      (∀ j, P.mulVec (f j) = lam j • f j) ∧
      (∀ j k, innerPi π (f j) (f k) = if j = k then 1 else 0) ∧
      ∀ (t : ℕ) (x y : V),
        (P ^ t) x y / π y = ∑ j, f j x * f j y * lam j ^ 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 12.1, Lemma 12.2, pp. 153-154

Read-back

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

Read-back: `spectral_representation`

Let $V$ be an arbitrary finite type with decidable equality, and write $n := |V|$ for its cardinality. The hypotheses are: $P$ is a $V \times V$ real matrix that is stochastic (every entry $P_{x,y} \ge 0$ and every row sums to one, $\sum_y P_{x,y} = 1$ ); $\pi : V \to \mathbb{R}$ is a distribution ( $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ ); additionally $\pi(x) > 0$ for every $x \in V$ (strict positivity, given as a separate hypothesis); and $P$ satisfies detailed balance with respect to $\pi$ : $\pi(x) P_{x,y} = \pi(y) P_{y,x}$ for all $x, y \in V$ . Note that $\pi$ is not assumed stationary for $P$ except insofar as detailed balance implies it; stationarity is not stated.

Under these hypotheses the theorem asserts the existence of a family of real numbers $\lambda_0, \dots, \lambda_{n-1}$ (indexed by $j \in \{0, \dots, n-1\}$ ) and a family of functions $f_0, \dots, f_{n-1} : V \to \mathbb{R}$ such that the following three statements hold simultaneously:

Eigenvector equations. For every index $j$ , the matrix–vector identity $P f_j = \lambda_j f_j$ holds, i.e. $\sum_y P_{x,y} f_j(y) = \lambda_j f_j(x)$ for all $x \in V$ . (No ordering of the $\lambda_j$ , no claim that $\lambda_0 = 1$ or that $f_0$ is constant, and no claim that the $\lambda_j$ exhaust or enumerate the spectrum is made.)
Orthonormality in the $\pi$ -weighted inner product. For all indices $j, k$ :

\langle f_j, f_k \rangle_\pi := \sum_{x \in V} f_j(x)\, f_k(x)\, \pi(x) \;=\; \begin{cases} 1 & j = k,\\ 0 & j \neq k. \end{cases}

(In particular each $f_j$ has $\pi$ -norm one, so each is nonzero, given that some $\pi(x) > 0$ — which forces $V$ to be nonempty for the hypotheses to be satisfiable together with $\sum_x \pi(x) = 1$ ; if $V$ were empty the sum-to-one condition in the distribution hypothesis would fail, making the theorem vacuously true for empty $V$ .)

Spectral representation of transition kernels. For every natural number $t$ (including $t = 0$ , where $P^0$ is the identity matrix) and all states $x, y \in V$ :

\frac{(P^t)_{x,y}}{\pi(y)} \;=\; \sum_{j=0}^{n-1} f_j(x)\, f_j(y)\, \lambda_j^{\,t},

where the left side is real division (with the convention $a/0 = 0$ , though $\pi(y) > 0$ is guaranteed here), and $\lambda_j^0 = 1$ by convention, including when $\lambda_j = 0$ .

The number of eigenpairs provided is exactly $n = |V|$ , matching the dimension. All three conclusions are packaged inside a single existential: the same families $(\lambda_j)$ and $(f_j)$ must witness all three at once.

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

Lemma 12.2 -- the spectral representation of a reversible chain

Read-back: spectral_representation

Read-back: `spectral_representation`