7.4 Hermite functions and the Hilbert basis of \(L^2(\mathbb {R})\)
The Hermite functions are \(h_n(x) = c_n H_n(x)\, e^{-x^2/4}\), where \(H_n\) is the probabilists’ Hermite polynomial (Mathlib’s Polynomial.hermite, monic, orthogonal for the weight \(e^{-x^2/2}\)) and \(c_n = \bigl(\sqrt{n!\, \sqrt{2\pi }}\bigr)^{-1}\) is derived so that the family is \(L^2\)-normalized for Lebesgue measure. The orthogonality relation \(\int H_m H_n e^{-x^2/2}\, dx = \delta _{mn}\, n!\, \sqrt{2\pi }\) is proved by induction from a Rodrigues-type recurrence, and yields \(\int h_m h_n\, dx = \delta _{mn}\). Each \(h_n\) is bundled as a Schwartz function (polynomial times Gaussian decay).
Any \(f \in L^2(\mathbb {R})\) with \(\langle h_n, f\rangle = 0\) for all \(n\) is zero. The analytic heart is Fourier-based: orthogonality to all \(h_n\) kills all moments of \(g = f \cdot e^{-x^2/4}\), hence (by dominated expansion of the Fourier kernel into its power series) \(\widehat{g} \equiv 0\), and \(L^1\)-Fourier injectivity gives \(g = 0\) a.e. Together with orthonormality this packages the Hermite functions as a HilbertBasis \(\mathbb {N} \to L^2(\mathbb {R})\), with the usual Fourier–Hermite expansion and Parseval identity.