Density of simple predictable processes for finite measures (source code)

= Density of simple predictable processes for finite measures
{title2=$\overline{\mathcal S}^{\,L^2(\mu)}=L^2(\mathcal P,\mu)$}

For every <finite measure> $\mu$ on the <predictable sigma-algebra>, bounded <simple predictable processes> are dense in $L^2(\mu)$. Include a bounded $\mathcal F_0$-measurable value supported at time zero when $\mu$ may charge that slice. Indicators of the generating rectangles and the <Pi-lambda theorem> prove density. This gives the completion step in the <Itô isometry> construction.