$L^2$ with the integral pairing is a Hilbert space

Real case: the pairing. For $f,g\in {\mathcal{L}}^2(\mu )$ the product $fg$ is integrable by [A1], so $\int fgd\mu$ is defined and depends only on the classes of $f$ and $g$ by [A1]; the assignment is bilinear by linearity of the integral on $L^1$ and symmetric because multiplication of real functions is commutative.

Complex case. The published complex interface [A4] states that on complex $L^2$ the pairing $\int f\bar{g}$ is representative-independent, linear in the first variable, conjugate-linear in the second, conjugate symmetric and positive definite with $⟨f,f⟩=\mathrm{\parallel }f{\mathrm{\parallel }}_2^2$, and that complex $L^2$ is complete for $\mathrm{\parallel }\cdot {\mathrm{\parallel }}_2$; hence complex $L^2(\mu ;\mathbb{C})$ is a complex Hilbert space for that pairing, with the established quotient norm.

The real pairing is positive definite: $⟨f,f⟩=\int f^{2}d\mu \ge 0$ vanishes exactly when $f^2=0$ almost everywhere, that is exactly when $f$ represents the zero class, by [A3]; moreover $⟨f,f⟩=\int f^{2}d\mu =\mathrm{\parallel }f{\mathrm{\parallel }}_2^2$ because the $L^2$ norm is the square root of $\int \mathrm{\mid }f{\mathrm{\mid }}^2$ and $f^2=\mathrm{\mid }f{\mathrm{\mid }}^2$ for real $f$. Hence the real pairing is an inner product inducing the quotient norm.

The real quotient is complete for that norm by [A2], so with this inner product real $L^2(\mu )$ is a real Hilbert space.

Steps 3.1 and 1.2 establish both claims for every measure space under Countable Choice, the norm in each case being the established quotient $L^2$ norm.