Optional Stopping Theorem

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

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.