L2 controls on a bounded spatial region form a separable Hilbert space

Define $Z:L^2(E)\to L^2({\mathbb{R}}^d)$ by zero extension and $R:L^2({\mathbb{R}}^d)\to L^2(E)$ by restriction. The maps are well-defined on almost-everywhere classes, $RZ$ is the identity on $L^2(E)$, and $\mathrm{\parallel }Rf{\mathrm{\parallel }}_{L^2(E)}\le \mathrm{\parallel }f{\mathrm{\parallel }}_{L^2({\mathbb{R}}^d)}$.

Let $\mathcal{S}$ be the countable dense rational box-step family from [F1]. The set $R(\mathcal{S})$ is countable. For $q\in L^2(E)$, choose any $\epsilon >0$ and extend it by $Zq$. By density there is $s\in \mathcal{S}$ with $\mathrm{\parallel }Zq-s{\mathrm{\parallel }}_{L^2({\mathbb{R}}^d)}<\epsilon$; then $\mathrm{\parallel }q-Rs{\mathrm{\parallel }}_{L^2(E)}=\mathrm{\parallel }R(Zq-s){\mathrm{\parallel }}_2\le \mathrm{\parallel }Zq-s{\mathrm{\parallel }}_2<\epsilon$. Thus $R(\mathcal{S})$ is dense in $L^2(E)$, proving separability.

The integral pairing makes $L^2(E)$ a real Hilbert space by [F3], so it is both separable and Hilbert. Countable Choice is the only stated choice principle in [F1] and [F3].