Conditional bracket isometry for stopped martingale increments (source code)

= Conditional bracket isometry for stopped martingale increments
{title2=$\mathbb E[(M_\tau-M_\sigma)^2\mid\mathcal F_\sigma]=\mathbb E([M]_\tau-[M]_\sigma\mid\mathcal F_\sigma)$}

For an <L2-bounded continuous martingale> and ordered possibly infinite <stopping times> $\sigma\leq\tau$, interpret the terminal stopped value as $M_\infty$. The <Doob L2 maximal inequality> bounds the expected squared path supremum. Localization of $M^2-[M]$ then gives $\mathbb E[M]_\infty<\infty$, so this square-minus-bracket local martingale has integrable supremum and is uniformly integrable. Apply the <optional stopping theorem> to it and to $M$. Expanding $(M_\tau-M_\sigma)^2$ makes the cross term vanish conditionally, proving the identity. Bounded $\mathcal F_\sigma$-measurable factors can be multiplied into either side.