Gaussian terminal value at a deterministic bracket level (source code)

= Gaussian terminal value at a deterministic bracket level
{c}
{title2=$[M]_T=a\Longrightarrow M_T\sim N(0,a)$}

Let $M$ be a zero-starting <continuous local martingale> and let $T<\infty$ be a <stopping time> with $[M]_{t\wedge T}\le a$ and $[M]_T=a$ for a deterministic $a$. The complex exponential $\exp(iuM_{t\wedge T}+u^2[M]_{t\wedge T}/2)$ is a bounded <local martingale>, hence a true <martingale>. Its terminal expectation is one, giving the <characteristic function> $\mathbb E e^{iuM_T}=e^{-u^2a/2}$. Conditional optional sampling between two bracket levels also gives independent Gaussian increments in inverse-bracket time; Gaussian one-time marginals alone do not establish that independence.