Weighted coefficient spaces form a Hilbert scale

Write $m=\mathrm{\mid }{I}_{\ast }\mathrm{\mid }$ and enumerate the basis by placing the finite family first, followed by $(\mathrm{\ell },k)$ at index $m+(2^{\mathrm{\ell }}-1)+k$, since $2^{\mathrm{\ell }}-1$ is the number of level indices below $\mathrm{\ell }$. For $x\in H_r$, define $T_{r}x$ by $(T_{r}x{)}_t=⟨x,e_{i_t}{⟩}_{H_0}$ for the finite coordinates and $(T_{r}x{)}_{m+(2^{\mathrm{\ell }}-1)+k}=2^{r\mathrm{\ell }}⟨x,e_{\mathrm{\ell }k}{⟩}_{H_0}$. Parseval [F1] gives $\mathrm{\parallel }{T}_{r}x{\mathrm{\parallel }}_{{\mathrm{\ell }}^2}^2=\mathrm{\parallel }x{\mathrm{\parallel }}_{H_r}^2$, so $T_r$ is an isometry into real ${\mathrm{\ell }}^2(\mathbb{N})$.

Given $b\in {\mathrm{\ell }}^2(\mathbb{N},\mathbb{R})$, set the finite-family coefficients equal to its first $m$ coordinates and put $a_{\mathrm{\ell }k}=2^{-r\mathrm{\ell }}{b}_{m+(2^{\mathrm{\ell }}-1)+k}$. Since $r\ge 0$, the sum of squares of all these coefficients is at most ${\sum }_n\mathrm{\mid }{b}_n{\mathrm{\mid }}^2<\mathrm{\infty }$. By [F3], their orthonormal expansion converges in $H_0$ to a vector $x$ with those coefficients. Thus $x\in H_r$ and $T_{r}x=b$, so $T_r$ is onto. By [F2], the isometric pullback of the real ${\mathrm{\ell }}^2$ inner product makes $H_r$ complete, and hence a real Hilbert space.

The finite-support rational sequences form a countable subset of real ${\mathrm{\ell }}^2$: each is encoded by a finite list of coordinate indices, integer numerators, and positive denominators, and such finite integer lists have an explicit natural-number encoding. Given $b\in {\mathrm{\ell }}^2$ and $\epsilon >0$, choose $N\ge 1$ so that $({\sum }_{n\ge N}\mathrm{\mid }{b}_n{\mathrm{\mid }}^2{)}^{1\mathrm{/}2}<\epsilon \mathrm{/}2$, then choose rationals $q_0,\dots ,q_{N-1}$ with $\mathrm{\mid }{b}_n-q_n\mathrm{\mid }<\epsilon \mathrm{/}(2\sqrt{N})$ for each $0\le n<N$, and set $q_n=0$ for $n\ge N$. Then $\mathrm{\parallel }b-q{\mathrm{\parallel }}_2^2={\sum }_{n<N}\mathrm{\mid }{b}_n-q_n{\mathrm{\mid }}^2+{\sum }_{n\ge N}\mathrm{\mid }{b}_n{\mathrm{\mid }}^2<{\epsilon }^2\mathrm{/}2<{\epsilon }^2$, so these finite-support rational sequences are dense. Because $T_r$ is an isometric bijection by steps 1.1 and 2.1, their inverse images are a countable dense subset of $H_r$. Hence $H_r$ is separable by [F4].

Each basis vector has a single nonzero coefficient, so its squared $H_r$ norm is $1$ on $I_{\ast }$ and $2^{2r\mathrm{\ell }}$ on level $\mathrm{\ell }$; distinct basis vectors are orthogonal under the weighted inner product. The finite-support coefficient vectors are dense by step 3.1, so the orthogonal family is complete in $H_r$. Finally Parseval [F1] gives $\mathrm{\parallel }x{\mathrm{\parallel }}_{H_0}^2={\sum }_{i\in I_{\ast }}\mathrm{\mid }⟨x,e_i⟩{\mathrm{\mid }}^2+{\sum }_{\mathrm{\ell },k}\mathrm{\mid }⟨x,e_{\mathrm{\ell }k}⟩{\mathrm{\mid }}^2\le \mathrm{\parallel }x{\mathrm{\parallel }}_{H_r}^2$ for $x\in H_r$, because $2^{2r\mathrm{\ell }}\ge 1$. Thus the inclusion has operator norm at most $1$.