Proposition 1.19 -- detailed balance implies stationarity

Open

MarkovMixing.detailed_balance_stationary

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

markov-chainsmixing-timesprobability

If a probability distribution $\pi$ satisfies the detailed balance equations $\pi(x)P(x,y)=\pi(y)P(y,x)$ for all states $x,y$ of a stochastic matrix $P$ , then $\pi$ is stationary for $P$ . This is the standard tool for identifying stationary distributions of reversible chains.

Preamble

import Definitions.Def_mm_basic

Formal statement

namespace MarkovMixing

/-- **Proposition 1.19** (LPW): any probability distribution satisfying the
detailed balance equations is stationary. -/
theorem detailed_balance_stationary {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (π : V → ℝ) (hπ : IsDist π)
    (hdb : DetailedBalance P π) :
    IsStationary P π := 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 1.6, Proposition 1.19, p. 14

Read-back

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

Let $V$ be an arbitrary finite type (of any universe) equipped with decidable equality; $V$ may be empty. Let $P$ be a $V \times V$ matrix with real entries, and assume $P$ is stochastic in the sense that every entry is nonnegative ( $0 \le P_{x,y}$ for all $x, y \in V$ ) and every row sums to one ( $\sum_{y \in V} P_{x,y} = 1$ for all $x \in V$ ; note that when $V$ is empty this row condition is vacuously true, since there are no rows). Let $\pi : V \to \mathbb{R}$ be a function assumed to be a distribution, meaning $\pi_x \ge 0$ for every $x \in V$ and $\sum_{x \in V} \pi_x = 1$ (a condition that is unsatisfiable when $V$ is empty, since the empty sum is $0 \ne 1$ , making the theorem vacuous in that case). Finally, assume the detailed-balance condition: for all $x, y \in V$ ,

\pi_x \, P_{x,y} = \pi_y \, P_{y,x}.

The theorem concludes that $\pi$ is stationary for $P$ , which by the bundle's definition is the conjunction of two claims: (i) $\pi$ is again a distribution (every value nonnegative and the values sum to one — a repetition of the hypothesis on $\pi$ ), and (ii) the row-vector–matrix product of $\pi$ with $P$ equals $\pi$ , i.e., for every $y \in V$ ,

\sum_{x \in V} \pi_x \, P_{x,y} = \pi_y.

No irreducibility, aperiodicity, or positivity of $\pi$ is assumed, and nothing is claimed about 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