Mean-zero square-integrable functions

Let $P$ be a probability measure on $(\mathcal{X},\mathcal{A})$. Here $L^2(P)$ is the real space of square-integrable measurable functions modulo equality $P$-almost surely, with its usual quotient norm (The space $L^p(\mu )$ as the quotient by null functions, The $L^p$ norm descends to the quotient and makes $L^p$ a normed space for $1\le p\le \mathrm{\infty }$). For $f\in L^2(P)$, the integral $Pf:=\int fdP$ is finite and independent of the representative: Cauchy–Schwarz on the probability space gives $\int \mathrm{\mid }f\mathrm{\mid }dP\le \mathrm{\parallel }f{\mathrm{\parallel }}_2$, and the expectation of integrable representatives is invariant under almost-sure equality (Cauchy-Schwarz inequality for $L^2$, Expectation depends only on the almost-everywhere class).

Define the mean-zero square-integrable space by

$L_0^2(P):=\{f\in L^2(P):Pf=0\}\mathrm{.}$

It carries the norm inherited from $L^2(P)$. Countable Choice is not needed for this definition; a later local Hilbert-space argument uses it only to inherit completeness from the library's general $L^2$ Hilbert-space result.