Continuous local martingale with bounded quadratic variation (source code)

= Continuous local martingale with bounded quadratic variation

A <continuous local martingale> $M$ with $M_0=0$ and deterministically bounded <quadratic variation> on every finite horizon is a <square-integrable> <martingale>, with $\mathbb EM_t^2=\mathbb E[M]_t$. Localization, the <Doob L2 maximal inequality>, and the resulting integrable bound on the squared supremum justify removing the <localizing sequence>.