Separable H1-zero space and compact L2 inclusion on a cube

Let $v\in C_c^{\mathrm{\infty }}(Q)$ and write $x=(t,x^{\mathrm{\prime }})$ with first library coordinate $t=x_0$ and $x^{\mathrm{\prime }}=(x_1,\dots ,x_{d-1})$ (the empty tuple when $d=1$). For fixed $x^{\mathrm{\prime }}$ and $0<t<1$, the one-dimensional fundamental theorem gives $v(t,x^{\mathrm{\prime }})={\int }_0^t{\mathrm{\partial }}_{0}v(s,x^{\mathrm{\prime }})ds$. Cauchy--Schwarz and $t\le 1$ imply $\mathrm{\mid }v(t,x^{\mathrm{\prime }}){\mathrm{\mid }}^2\le {\int }_0^1\mathrm{\mid }{\mathrm{\partial }}_{0}v(s,x^{\mathrm{\prime }}){\mathrm{\mid }}^{2}ds$. Integrating first in $t$ and then in $x^{\mathrm{\prime }}$ gives $\mathrm{\parallel }v{\mathrm{\parallel }}_2^2\le \mathrm{\parallel }{\mathrm{\partial }}_{0}v{\mathrm{\parallel }}_2^2$. By [F1], approximating any $v\in H_0^1(Q)$ in $H^1$ and passing to the limit proves the displayed Poincaré bound.

The map $J:H^1(Q)\to L^2(Q{)}^{d+1}$, $J(v)=(v,{\mathrm{\partial }}_{0}v,\dots ,{\mathrm{\partial }}_{d-1}v)$, is an isometry for the Sobolev norm by [F1]. The target is separable: extend each coordinate by zero to ${\mathbb{R}}^d$ and restrict the countable dense rational-box family [F3]. The image $J(H^1(Q))$ and its subset $J(H_0^1(Q))$ are separable subspaces of a second-countable metric space: intersect a countable base with the subspace and choose one point from each nonempty basic set, a countable selection allowed by Countable Choice. Thus $H_0^1(Q)$ is separable.

For $v\in C_c^{\mathrm{\infty }}(Q)$, extend it by zero to $D=(-1,2{)}^d$ and identify opposite faces of $D$ to obtain a smooth function on the torus of side length $3$. The extension preserves the $H^1$ norms. By [F1], for every $v\in H_0^1(Q)$ choose test functions converging to $v$ in $H^1$; their periodic zero extensions are Cauchy in $H^1$ on this torus, so the extension is in periodic $H^1(D)$ and the same norm bound holds.

Rescale $D$ affinely to the unit torus using [F7]; the characters on the side-length-$3$ torus are $e^{2\pi ik\cdot x\mathrm{/}3}$. For a periodic $H^1(D)$ function $V$, integration by parts on smooth periodic approximants and passage in $H^1$ give $\widehat{{\mathrm{\partial }}_{j}V}(k)=(2\pi i{k}_j\mathrm{/}3)\widehat{V}(k)$ for $0\le j<d$. The zero extension in step 1.3 is supported away from the identified faces, so its weak derivatives on the torus are exactly its zero-extended weak derivatives on $Q$. Parseval [F4] therefore yields ${\sum }_{k\in {\mathbb{Z}}^d}(1+\mathrm{\mid }k{\mathrm{\mid }}^2)\mathrm{\mid }\widehat{V}(k){\mathrm{\mid }}^2\le C_d\mathrm{\parallel }V{\mathrm{\parallel }}_{H^1(D)}^2$, with a fixed constant accounting for the side length $3$. Hence for every integer $N\ge 1$, ${\sum }_{\mathrm{\mid }k\mathrm{\mid }>N}\mathrm{\mid }\widehat{V}(k){\mathrm{\mid }}^2\le C_d{N}^{-2}\mathrm{\parallel }V{\mathrm{\parallel }}_{H^1(D)}^2$.

Let $(v_n)$ be bounded in $H_0^1(Q)$, and write $V_n$ for the periodic zero extensions from step 1.3. For each fixed Fourier mode $k$, the complex coefficients are bounded, so their real and imaginary parts are bounded real sequences. Use the following fixed extraction rule for any bounded real sequence $(b_n)$: let $m$ be the least positive integer bounding all $\mathrm{\mid }{b}_n\mathrm{\mid }$, start with $[-m,m]$, and bisect repeatedly, keeping the left closed half if it contains infinitely many terms and otherwise the right closed half. At stage $r$ take the least index larger than the previous index whose term lies in the retained interval. Each such index exists, and the selected terms are Cauchy because the intervals are nested with lengths tending to zero; [F5] then implies they converge. This defines a unique subsequence from the input sequence, without choice. Enumerate the real and imaginary parts of the Fourier modes, recursively apply this fixed rule to the current subsequence for the next coordinate, and let $n_r$ be the $r$th index of the $r$th nested subsequence. These diagonal indices increase strictly and form a tail subsequence of every fixed earlier extraction, so every coefficient converges; this recursion uses a specified function, not Dependent Choice. If its terms are $V_{n_r},V_{n_s}$, then for fixed $N$ the sum of squared coefficient differences over $\mathrm{\mid }k\mathrm{\mid }\le N$ tends to zero as $r,s\to \mathrm{\infty }$, while by step 2.1 the sum over $\mathrm{\mid }k\mathrm{\mid }>N$ is at most $C{N}^{-2}$ uniformly in $r,s$. First choose $N$ large, then $r,s$ large; Parseval shows $(V_{n_r})$ is Cauchy in $L^2(D)$. Completeness gives an $L^2(D)$ limit, and restriction to $Q$ gives the required $L^2(Q)$ convergence.