Mean-square completion of trigonometric polynomials (source code)

= Mean-square completion of trigonometric polynomials
{title2=$H_M$}

Start with finite real linear combinations of $1$, $\cos(\lambda x)$ and $\sin(\lambda x)$ with arbitrary positive real frequencies, and use the <inner product> $\langle f,g\rangle_M=\lim_{R\to\infty}R^{-1}\int_{-R}^Rfg$. Product-to-sum identities give existence of these averages and mutual <orthogonality> of distinct frequencies. The squared <norm> is $2a_0^2+\sum_\lambda(a_\lambda^2+b_\lambda^2)$. Its <Hilbert space completion> contains an uncountable <orthonormal set>, so is not a <separable Hilbert space>. This construction does not equip all <locally square-integrable functions> with an <inner product>: compactly supported nonzero functions have zero mean square, and other functions have divergent or nonexistent averages.