$W^{1,2}(S^1,\mathbb{R}^{2n})$ has trivial orthogonal complement in $L^2(S^1,\mathbb{R}^{2n})$

Let $S^1=\mathbb R/\mathbb Z$ with its Haar probability measure and let $L^2_n=L^2(S^1,\mathbb R^{2n})$. For $f\in L^2_n$ and $k\in\mathbb Z$ let $\hat f_k=\int_{S^1}e^{-2\pi ikt}f(t)\,dt\in\mathbb C^{2n}$ be its $k$-th Fourier coefficient, computed componentwise after viewing the real entries of $f$ as complex numbers.

Say $f\in W^{1,2}$ if $\sum_{k\in\mathbb Z}(1+k^2)|\hat f_k|^2<\infty$. If $g\in L^2_n$ satisfies $\langle f,g\rangle_{L^2}=\int_{S^1}\langle f(t),g(t)\rangle\,dt=0$ for every $f\in W^{1,2}$, then $g=0$.

Equivalently, the orthogonal complement of $W^{1,2}(S^1,\mathbb R^{2n})$ in $L^2(S^1,\mathbb R^{2n})$ is zero, so every linear subspace of $L^2_n$ containing $W^{1,2}$ is dense. This is the density half of the description of the domain of the asymptotic operator $A_S=-J_0\partial_t-S$.

Formalization note: L2 n, coeff and InW12 come from the definition module AsymptoticOperator_Setting; L2 n is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 over UnitAddCircle with AddCircle.haarAddCircle, InW12 f is the summability condition above, and inner ℝ f g is the $L^2$ inner product.