I have a question regarding separability of a certain locally convex space.
Let $H_{\tau}:=H^{\tau_1}(\mathbb{R}^n,\tau_2(x)dx)$ the weighted Sobolev Hilbert space with $\tau_1 \in \mathbb{N}, \tau_2(x)\in C^\infty(\mathbb{R}^n)$ and with $\tau_2 \ge 1$.
We denote $\mathcal{D}(\mathbb{R}^n)=\bigcap_\tau H_\tau$, when $\tau$ is arbitrary with stated properties above (and call $T$ the index set of all these $\tau$), endowed with the projective topology with respect to all the embeddings $\iota_\tau: \mathcal{D}(\mathbb{R}^n) \longrightarrow H_\tau$, i.e. the coarsest topology for which all these embeddings are continuous. This space is a nuclear and separable. The following construction will be the case when $n=1$.
Also consider the symmetrical Fock spaces
$$\mathcal{F}(H_\tau):=\bigoplus^\infty_{k=0}H_{\tau, \mathbb{C}}^{\hat \otimes k}$$
of nth-symmetrized Hilbert space tensor products of the Sobolev spaces introduced above. This is the direct sum in of a countable collection of Hilbert spaces. We now consider the weighted Fock spaces
$$\mathcal{F}(H_\tau,p)=\lbrace (f_n) \in \mathcal{F}(H_\tau):\sum_n \|f_n\|^2_{H_{\tau,\mathbb{C}}^{\hat \otimes n}}\cdot p_n < \infty \rbrace,$$
for sequences $(p_n)$ with $p_n\ge 1$ for all $n\in \mathbb{N}$.
The space I am interested in is
$$\mathcal{F}_{\text{fin}}(\mathcal{D})=\bigcap\limits_{\tau \in T, p\ge 1 } \mathcal{F}(H_\tau,p)$$
the locally convex space as the projective limit of the weighted Fock spaces endowed with the projective topology, i.e. the initial topology with respect to all the embeddings $\iota_{\tau, p}:\mathcal{F}_{\text{fin}}(\mathcal{D}) \longrightarrow \mathcal{F}(H_\tau,p)$. I am wondering why this space is separable..
The separability is necessary to apply the so called projection spectral theorem in its most general form see [Y.M. Berezansky et al. Spectral Methods in Infinite-Dimensional Analysis, Chapter 3, Theorem 2.7]. This space gets used in the paper [Yu. M. Berezansky and V. A. Tesko. “The investigation of Bogoliubov func- tionals by operator methods of moment problem”. In: Methods Funct. Anal. Topology 22.1 (2016), pp. 1–47. issn: 1029-3531] as if it is separable, but the author does not specify why this is the case.
My current thoughts lead to the following:
If I can show, that
$$\bigcap_{\tau \in T}(H^{\tau_1}(\mathbb{R},\tau_2(x)dx))^{\otimes n}=\bigcap_{\tau \in T}H^{\tau_1}(\mathbb{R}^n,\tau_2(x)dx)=\mathcal{D}(\mathbb{R}^n),$$
then $\mathcal{F}_{\text{fin}}(\mathcal{D})=\bigoplus_k \mathcal{D}(\mathbb{R}^k)_{\text{symm},\mathbb{C}}$ as a set, i.e. the set of all finite sequences. And since $\mathcal{D}(\mathbb{R}^k)$ is separable for all $k \in \mathbb{N}$, we can conclude $$\bigoplus_k \mathcal{D}(\mathbb{R}^k)_{\text{symm},\mathbb{C}}$$ is separable as a topological sum. Now If we additionally show that the topology of the sum is finer, than the topology of the projective limit, we are done.
Is there a dense and continuous inclusion
$$H^{\tau_1}(\mathbb{R}^2,\tau_2(x)dx)\subseteq H^{\tau_3}(\mathbb{R},\tau_4(x)dx)\otimes H^{\tau_3}(\mathbb{R},\tau_4(x)dx) \subseteq H^{\tau_3}(\mathbb{R}^2,\tau_4(x)dx)$$
for any pair $(\tau_3, \tau_4) \in T$? This could inductivly show
$$\bigcap_{\tau \in T}(H^{\tau_1}(\mathbb{R},\tau_2(x)dx))^{\otimes n}=\bigcap_{\tau \in T}H^{\tau_1}(\mathbb{R}^n,\tau_2(x)dx)=\mathcal{D}(\mathbb{R}^n).$$
