$\pi(S_t)$ is a martingale

Proved

MarkovMixing.evolving_sets_martingale

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ with strictly positive stationary distribution $\pi$ , and write $Q(S,y)=\sum_{x\in S}\pi(x)P(x,y)$ for the stationary flow from a set $S$ into a state $y$ . The evolving-set process is the Markov chain on subsets of $V$ that, from $S$ , draws $u$ uniform on $(0,1]$ and passes to the superlevel set $\{y:Q(S,y)/\pi(y)\ge u\}$ ; its transition probability from $S$ to $T$ is the length of the interval of thresholds realizing $T$ . A process adapted to a chain is a martingale when its one-step conditional expectation is neutral (the pointwise finite-sum identity of this mission's definitions).

The theorem (Lemma 17.13 of Levin–Peres–Wilmer) asserts that the stationary mass of the evolving set,

M_t\;=\;\pi(S_t)\;=\;\sum_{v\in S_t}\pi(v),

is a martingale for the evolving-set process: for every set $S$ , $\;\sum_TK(S,T)\,\pi(T)=\pi(S)$ , where $K$ is the process's transition matrix.

The mass gained when the threshold $u$ is small exactly balances the mass lost when it is large — stationarity of $\pi$ in disguise. This martingale is the engine of the whole chapter: the goal theorem controls the square root $\sqrt{\pi(S_t)}$ as a strict supermartingale whose decay rate is the bottleneck constant, and optional stopping converts that decay into mixing bounds.

Preamble

import Definitions.Def_mm_martingale

Formal statement

namespace MarkovMixing

/-- **Lemma 17.13** (LPW): for the evolving-set process, the sequence
`π(S_t)` is a martingale. -/
theorem evolving_sets_martingale {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary P π) (hpos : ∀ x : V, 0 < π x) :
    IsChainMartingale (evolvingSets P π)
      (fun t ω => ∑ v ∈ ω (Fin.last t), π v) := 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, Lemma 17.13, p. 236

Read-back

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

Read-back: evolving_sets_martingale

Let $V$ be a finite type with decidable equality, let $P$ be a real matrix on $V\times V$ that is stochastic (all entries nonnegative, every row summing to $1$ ), and let $\pi : V \to \mathbb{R}$ be stationary for $P$ (i.e. $\pi$ is a probability distribution — nonnegative, summing to $1$ — and the row vector $\pi$ satisfies $\pi P = \pi$ ) with $\pi_v > 0$ for every $v \in V$ .

Let $K$ be the evolving-set matrix of $(P,\pi)$ , a real matrix indexed by all subsets of $V$ , with entries

K(S,T) \;=\; \max\bigl(0,\ U(S,T) - L(S,T)\bigr),

where, with the clamped threshold $\widehat{Q}(S,z) = \min\bigl(1, \max\bigl(0, \tfrac{\sum_{u \in S}\pi_u P(u,z)}{\pi_z}\bigr)\bigr)$ (total real division, never dividing by zero here since $\pi$ is strictly positive), $U(S,T)$ is the minimum of $\widehat{Q}(S,\cdot)$ over $T$ (or $1$ if $T = \varnothing$ ) and $L(S,T)$ is the maximum of $\widehat{Q}(S,\cdot)$ over the complement of $T$ (or $0$ if $T = V$ ).

The theorem asserts that the family $M_t(\omega) = \pi\bigl(\omega_t\bigr) := \sum_{v \in \omega_t} \pi_v$ — assigning to each path $\omega : \{0,\dots,t\} \to \{\text{subsets of } V\}$ the $\pi$ -mass of its last entry — is a chain martingale with respect to the matrix $K$ on the state space of subsets of $V$ . Unfolding that definition, the assertion is: for every $t \in \mathbb{N}$ and every sequence of subsets $\omega_0, \dots, \omega_t \subseteq V$ (arbitrary — no positivity of the path's weight under $K$ is required, and only the last entry $\omega_t$ actually enters the equation),

\sum_{T \subseteq V} K(\omega_t, T)\; \pi(T) \;=\; \pi(\omega_t),

where the sum runs over all subsets $T$ of $V$ (including $\varnothing$ , for which $\pi(\varnothing) = 0$ , and $V$ itself, for which $\pi(V) = 1$ ). Equivalently: for every subset $S \subseteq V$ , $\sum_{T} K(S,T)\,\pi(T) = \pi(S)$ . Nothing in the statement asserts that $K$ is a stochastic matrix; the claim is exactly this one-step averaging identity for the specific functional " $\pi$ -mass of the current set".

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

π(St)\pi(S_t)π(St​) is a martingale

Read-back: evolving_sets_martingale

$\pi(S_t)$ is a martingale