Email Gateway (Jun 12 2026 at 15:41): Email Gateway (Jun 12 2026 at 15:41):From: Manuel Eberl <manuel@pruvisto.org>
Fair Games Theorem
by Lawrence C. Paulson
This is the optional stopping theorem (or fair games theorem) for
real-valued discrete-time stochastic processes on a σ-finite filtered
measure space. A theory of piecewise-constant stopping times – the
function taking i on an F_i-measurable set S and j on its complement –
is developed, together with the corresponding decomposition of integrals
over the two pieces. The central results then prove both directions of
the theorem: if X is a submartingale, then for any bounded stopping
times τ ≤ π the expected stopped values satisfy E[X_τ] ≤ E[X_π] (via the
telescoping identity and the submartingale set-integral inequality);
conversely, monotonicity of expected stopped values over all bounded
stopping times characterises submartingales. It is further shown that
the stopped process X^τ of a submartingale is again a submartingale.
Throughout, the theorems are cross-referenced to their counterparts in
Mathlib's OptionalStopping, from which it was translated by Claude. It
was polished manually afterwards.
The fair games theorem is #62 on the Top 100 Mathematical Theorems.
https://isa-afp.org/entries/Fair_Games_Theorem.html
Enjoy,
Manuel
Last updated: Jul 02 2026 at 07:34 UTC