Dyadic conditional averages recover integrable functions (source code)

= Dyadic conditional averages recover integrable functions
{title2=$f_n\to f\text{ almost everywhere and in }L^1$}

For an integrable <function> on $[0,1]$, average $f$ on each <dyadic interval> of length $2^{-n}$. The resulting <step function> $f_n$ converges to $f$ <almost everywhere> and in the <L1 norm>. If $U$ has the <uniform distribution> on $[0,1]$, then $f_n(U)=\mathbb E[f(U)\mid\sigma(b_n(U))]$, where $b_n$ rounds down to a dyadic endpoint. Refinement makes these <conditional expectations> a <uniformly integrable> <martingale>. The <uniformly integrable martingale convergence theorem> gives almost-sure and <convergence in L1> to a limit $Y$.

Since $b_n(U)\to U$, the generated limiting <sigma-algebra> contains $U$ up to null sets. For every <event> $A$ in any finite-stage <sigma-algebra>, convergence in the <L1 norm> gives $\mathbb E[Y\mathbf1_A]=\mathbb E[f(U)\mathbf1_A]$. The <pi-lambda theorem> extends this equality to the limiting <sigma-algebra>, identifying $Y=f(U)$. The <uniform distribution> of $U$ translates the two convergence conclusions into the assertions for $f_n$. Choosing a Borel representative of $f$ and assigning arbitrary values at the endpoint one makes all random variables well defined without changing either conclusion.