$H^k$ is a Hilbert space under the derivative-sum inner product

By [F17] the given Axiom of Choice [F18] yields Countable Choice, so the Countable-Choice conventions under which [F1], [F2] and [F19] are stated are in force. Hence the notation $H^k(\mathrm{\Omega };\mathbb{K})=W^{k,2}(\mathrm{\Omega };\mathbb{K})$ of [F1] is available; by [F2] every class of $H^k(\mathrm{\Omega };\mathbb{K})$ lies in $L^2(\mathrm{\Omega };\mathbb{K})$ and each $D^{\alpha }u$, $\alpha \in {\mathcal{A}}_k$, is again an $L^2(\mathrm{\Omega };\mathbb{K})$ class; by [F3] the index set ${\mathcal{A}}_k$ is finite and nonempty, so it can be enumerated as ${\alpha }_1,\dots ,{\alpha }_m$ with $m\ge 1$; by [F4] $D^{0}u=u$; by [F5] the displayed $W^{k,2}$ norm is the square root of ${\sum }_{\alpha \in {\mathcal{A}}_k}\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_{L^2(\mathrm{\Omega })}^2$; and by [F7] $H^k(\mathrm{\Omega };\mathbb{K})$ with that norm is a complete normed space over $\mathbb{K}$, in particular a $\mathbb{K}$-vector space.

Assume first that $\mathbb{K}=\mathbb{C}$. Applying the finite-tuple clause of [F6] to the tuple $F=(D^{{\alpha }_1}u,\dots ,D^{{\alpha }_m}u)$ and $G=(D^{{\alpha }_1}v,\dots ,D^{{\alpha }_m}v)$ gives that $B(u,v):={\sum }_{j=1}^m⟨D^{{\alpha }_j}u,D^{{\alpha }_j}v⟩={\sum }_{\alpha \in {\mathcal{A}}_k}{\int }_{\mathrm{\Omega }}{D}^{\alpha }u\overline{D^{\alpha }v}dx$ is representative-independent and finite, is linear in the first tuple slot, is conjugate-linear in the second, is conjugate-symmetric, and is positive definite, with $B(u,u)={\sum }_{\alpha \in {\mathcal{A}}_k}\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_2^2$. If $w\in H^k(\mathrm{\Omega };\mathbb{C})$ and $a,b\in \mathbb{C}$, then [F19] applied coordinatewise gives $D^{\alpha }(au+bw)=a{D}^{\alpha }u+b{D}^{\alpha }w$ weakly for every $\alpha \in {\mathcal{A}}_k$; the right-hand side lies in $L^2(\mathrm{\Omega };\mathbb{C})$, so it is the same class as $D^{\alpha }(au+bw)$ by [F2], and the tuple slot is complex-linear in the class. Therefore $B$ is linear in the first variable and conjugate-linear in the second as a function on $H^k(\mathrm{\Omega };\mathbb{C})\times H^k(\mathrm{\Omega };\mathbb{C})$, and $B(u,u)=0$ forces $D^{\alpha }u=0$ for every $\alpha$ by the positivity in [F6], in particular $u=D^{0}u=0$ by [F4]. By the axiom list [F8] the pairing $B$ is an inner product on the complex vector space $H^k(\mathrm{\Omega };\mathbb{C})$ of step 1.1, with $B(u,u)={\sum }_{\alpha \in {\mathcal{A}}_k}\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_2^2$.

Assume now that $\mathbb{K}=\mathbb{R}$. For each $\alpha \in {\mathcal{A}}_k$ choose a measurable real representative $f_{\alpha }$ of the class $D^{\alpha }u$ and $h_{\alpha }$ of the class $D^{\alpha }v$; this is a selection from finitely many nonempty sets, so it needs no choice principle. By [F11] with $p=q=2$ each product $f_{\alpha }{h}_{\alpha }$ is integrable, and by [F13] the number ${\int }_{\mathrm{\Omega }}{f}_{\alpha }{h}_{\alpha }$ depends only on the two almost-everywhere classes. Setting $B(u,v):={\sum }_{\alpha \in {\mathcal{A}}_k}{\int }_{\mathrm{\Omega }}{D}^{\alpha }u{D}^{\alpha }vdx$ therefore defines a finite, representative-independent pairing. If $a,b\in \mathbb{R}$ and $w\in H^k(\mathrm{\Omega };\mathbb{R})$ with representatives $g_{\alpha }$ of $D^{\alpha }w$, then [F19] makes $a{f}_{\alpha }+b{g}_{\alpha }$ a representative of $D^{\alpha }(au+bw)$, and [F12] yields $\int (a{f}_{\alpha }+b{g}_{\alpha })h_{\alpha }=a\int f_{\alpha }{h}_{\alpha }+b\int g_{\alpha }{h}_{\alpha }$ and likewise in the second variable; also $\int f_{\alpha }{h}_{\alpha }=\int h_{\alpha }{f}_{\alpha }$. Hence $B$ is bilinear and symmetric on $H^k(\mathrm{\Omega };\mathbb{R})\times H^k(\mathrm{\Omega };\mathbb{R})$. Since the $f_{\alpha }$ are real, [F15] and [F16] give ${\int }_{\mathrm{\Omega }}{f}_{\alpha }^2=\mathrm{\parallel }{f}_{\alpha }{\mathrm{\parallel }}_2^2=\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_2^2\ge 0$, so $B(u,u)={\sum }_{\alpha \in {\mathcal{A}}_k}\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_2^2$; if this is $0$, then every $f_{\alpha }$ vanishes almost everywhere by [F14], in particular $u=D^{0}u=0$ by [F4], while $u=0$ plainly gives $B(u,u)=0$. By [F8] the pairing $B$ is an inner product on the real vector space $H^k(\mathrm{\Omega };\mathbb{R})$ of step 1.1.

In the complex case, [F9] says that the norm induced by the inner product $B$ of step 2.1 is $\mathrm{\parallel }u\mathrm{\parallel }=\sqrt{B(u,u)}=({\sum }_{\alpha \in {\mathcal{A}}_k}\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_2^2{)}^{1\mathrm{/}2}$, which by [F5] is exactly the displayed $W^{k,2}$ norm of $u$ for $p=2$. By [F7] with $p=2$ the space $W^{k,2}(\mathrm{\Omega };\mathbb{C})$ is complete for that displayed norm, so the induced-length metric of $H^k(\mathrm{\Omega };\mathbb{C})$ is complete, and [F10] makes $H^k(\mathrm{\Omega };\mathbb{C})$ a complex Hilbert space.

In the real case the same computation with step 2.2 gives $\mathrm{\parallel }u\mathrm{\parallel }=({\sum }_{\alpha \in {\mathcal{A}}_k}\mathrm{\parallel }{D}^{\alpha }u{\mathrm{\parallel }}_2^2{)}^{1\mathrm{/}2}$ equal to the displayed $W^{k,2}$ norm by [F5], and [F7] with $p=2$ plus [F10] make $H^k(\mathrm{\Omega };\mathbb{R})$ a real Hilbert space.

Combining steps 2.1 and 2.2, the single displayed formula defines an inner product on $H^k(\mathrm{\Omega };\mathbb{K})$, linear in the first variable, for each of the two scalar fields, and steps 3.1 and 3.2 identify its induced norm with the displayed $W^{k,2}$ norm and its induced-length metric as complete; hence $H^k(\mathrm{\Omega };\mathbb{K})$ is a Hilbert space over $\mathbb{K}$ in the sense of [F10]. At $k=0$ the sum has the single term $\alpha =0$, so the pairing is the $L^2$ pairing ${\int }_{\mathrm{\Omega }}u\bar{v}$, the norm identity is the $W^{0,2}=L^2$ case of [F4] and [F5], and the completeness assertion is the $p=2$, $k=0$ case of [F7]; at $k\ge 1$ all finitely many summands are present. If $\mathrm{\Omega }=\mathrm{\varnothing }$, then by [F1] and [F4] the only class is zero and every summand vanishes, so $H^k(\mathrm{\varnothing };\mathbb{K})=\{0\}$ is a Hilbert space. The only choice principle used is the given Axiom of Choice [F18], spent through Countable Choice obtained in step 1.1 by [F17] and through the completeness interface [F7]; the enumeration ${\alpha }_1,\dots ,{\alpha }_m$ of [F3] and the representative selections in step 2.2 are finite and choice-free, and no representative selection for infinitely many classes occurs. $\mathrm{\square }$