Optional Stopping Theorem

Proved

MarkovMixing.optional_stopping

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$ . A martingale adapted to the chain is a family $M_t$ of real-valued functions of the trajectory up to time $t$ whose one-step conditional expectation is neutral: $\sum_yP(\omega_t,y)\,M_{t+1}(\omega,y)=M_t(\omega)$ for every trajectory $\omega$ , where $(\omega,y)$ extends $\omega$ by one step. A stopping time $\tau$ is a $\{0,1\}$ -valued stopping rule: whether to stop at time $t$ is determined by the trajectory up to $t$ . Fix a starting state $x$ ; $\tau$ is almost surely finite when the total probability of ever stopping equals one, and the stopped expectation $\mathbb E_x(M_\tau)$ is the sum over all times $t$ and trajectories from $x$ of (trajectory weight) × (probability of stopping exactly at $t$ ) × $M_t$ .

The theorem (the Optional Stopping Theorem, Corollary 17.7 of Levin–Peres–Wilmer) asserts: if $M$ is uniformly bounded — $|M_t(\omega)|\le K$ for some constant $K$ and all $t,\omega$ — and $\tau$ is almost surely finite, then

\mathbb E_x\bigl(M_{\tau}\bigr)\;=\;M_0(x):

stopping a fair game at a fair time wins nothing. This identity is the workhorse of discrete probability — the gambler's ruin probabilities and hitting-time identities of Missions I and VI are all instances — and in this mission it feeds the analysis of the evolving-set process.

Preamble

import Definitions.Def_mm_martingale

Formal statement

namespace MarkovMixing

/-- **Corollary 17.7, the Optional Stopping Theorem** (LPW): if `M` is a
bounded martingale with respect to the chain and `τ` is an almost surely
finite stopping time, then `E_x(M_τ) = M_0(x)`. -/
theorem optional_stopping {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (M : ∀ t : ℕ, (Fin (t + 1) → V) → ℝ) (hM : IsChainMartingale P M)
    (s : ∀ t : ℕ, (Fin (t + 1) → V) → ℝ)
    (hs01 : ∀ (t : ℕ) (ω : Fin (t + 1) → V), s t ω = 0 ∨ s t ω = 1)
    (x : V) (hfin : (∑' t : ℕ, ∑ y, stopAtProb P x s t y) = 1)
    (K : ℝ) (hK : ∀ (t : ℕ) (ω : Fin (t + 1) → V), |M t ω| ≤ K) :
    stoppedExp P x s M = M 0 (fun _ => x) := 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.2, Corollary 17.7 (Optional Stopping Theorem, Version 2), p. 232

Read-back

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

Read-back: optional_stopping

Let $V$ be a finite type with decidable equality (possibly empty), and let $P$ be a real matrix on $V \times V$ that is stochastic: every entry satisfies $P(x,y) \ge 0$ and every row sums to $1$ , i.e. $\sum_y P(x,y) = 1$ for each $x$ . Let $M$ be a family assigning a real number $M_t(\omega)$ to each $t \in \mathbb{N}$ and each path $\omega : \{0,\dots,t\}\to V$ , and assume $M$ is a chain martingale for $P$ : for every $t$ and every path $\omega$ of length $t+1$ ,

\sum_{y \in V} P(\omega_t, y)\, M_{t+1}(\omega \frown y) = M_t(\omega),

where $\omega \frown y$ appends $y$ to $\omega$ . Let $s$ be a family assigning a real number $s_t(\omega)$ to each $t$ and each path $\omega$ of length $t+1$ , and assume each value is exactly $0$ or exactly $1$ (this is the only constraint on $s$ ; nothing requires $s$ to depend on the path in any adapted way beyond its type, which already forces $s_t$ to depend only on the first $t+1$ states). Fix a starting state $x \in V$ . Write, for $t \in \mathbb{N}$ and $y \in V$ ,

p_t(y) \;=\; \sum_{\substack{\omega : \{0,\dots,t\}\to V \\ \omega_0 = x,\ \omega_t = y}} \left(\prod_{i=0}^{t-1} P(\omega_i,\omega_{i+1})\right)\left(\prod_{u=0}^{t-1}\bigl(1 - s_u(\omega|_{\{0,\dots,u\}})\bigr)\right) s_t(\omega)

for the probability-like mass of stopping at time $t$ in state $y$ starting from $x$ (a finite sum over all paths; $\omega|_{\{0,\dots,u\}}$ is the length- $(u+1)$ prefix; both products are empty, hence $1$ , when $t=0$ ). Assume the hypothesis

\sum_{t=0}^{\infty} \sum_{y\in V} p_t(y) \;=\; 1,

where the sum over $t$ is a tsum (equal to $0$ by convention if the family is not summable — the hypothesis rules that degenerate reading out, since it asserts the value is $1$ ). Finally, assume there is a real number $K$ (its sign is not separately hypothesized) with $|M_t(\omega)| \le K$ for all $t$ and all paths $\omega$ .

Then the theorem asserts the equality

\sum_{t=0}^{\infty}\ \sum_{\substack{\omega : \{0,\dots,t\}\to V \\ \omega_0 = x}} \left(\prod_{i=0}^{t-1} P(\omega_i,\omega_{i+1})\right)\left(\prod_{u=0}^{t-1}\bigl(1 - s_u(\omega|_{\{0,\dots,u\}})\bigr)\right) s_t(\omega)\, M_t(\omega) \;=\; M_0(\bar x),

where the left-hand side's outer sum over $t$ is again a tsum (value $0$ if not summable), and $\bar x$ denotes the one-point path of length $1$ constantly equal to $x$ . In words: the stopped expectation of $M$ — the sum over all times $t$ and all paths from $x$ of (path weight) × (product of one-minus- $s$ over all proper prefixes) × ( $s$ at time $t$ ) × ( $M$ at time $t$ ) — equals the initial value $M_0$ at the trivial path sitting at $x$ . If $V$ is empty, the hypothesis $\sum_t \sum_y p_t(y) = 1$ is unsatisfiable (every inner sum is empty, so the total is $0$ ), making the statement vacuous in that case.

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