Parseval and expansions for the Gaussian Hermite basis

TauCeti.gaussianHermiteHilbertBasis exhibits the normalized probabilists' Hermite polynomials Hₙ / √(n!) as a Hilbert basis of L²(N(0, 1); 𝕜). This file supplies the coefficient, Parseval, and reconstruction API for that basis. In particular, its coordinate theorem writes the abstract HilbertBasis.repr coordinate as the Gaussian integral against Hₙ / √(n!).

Main statements

• TauCeti.gaussianHermiteHilbertBasis_repr_apply identifies each coordinate with its integral.
• TauCeti.tsum_norm_sq_integral_hermite_mul_gaussianReal is Parseval's identity for those coefficients.
• TauCeti.summable_norm_sq_integral_hermite_mul_gaussianReal gives square-summability of the coefficients.
• TauCeti.hasSum_gaussianHermite_expansion reconstructs every L² vector from its Gaussian Hermite series.

The coefficient itself has no name of its own: it is spelled out as the integral against Hₙ / √(n!), so the two Parseval-side lemmas are named after that integral, as TauCeti.memLp_hermite_gaussianReal names the same normalized integrand.

All statements hold for an arbitrary RCLike scalar field, simultaneously covering real and complex-valued L² functions.

@[simp]

theorem TauCeti.gaussianHermiteHilbertBasis_repr_apply {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))) (n : ℕ) : ↑((gaussianHermiteHilbertBasis 𝕜).repr f) n = ∫ (x : ℝ), (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial) * ↑↑f x ∂ProbabilityTheory.gaussianReal 0 1

The n-th Gaussian Hermite coordinate is the integral of f against the normalized probabilists' Hermite polynomial Hₙ / √(n!).

theorem TauCeti.tsum_norm_sq_integral_hermite_mul_gaussianReal {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))) : ∑' (n : ℕ), ‖∫ (x : ℝ), (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial) * ↑↑f x ∂ProbabilityTheory.gaussianReal 0 1‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the Gaussian Hermite basis. The squared norms of the Gaussian Hermite coefficients of f sum to ‖f‖².

theorem TauCeti.summable_norm_sq_integral_hermite_mul_gaussianReal {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))) : Summable fun (n : ℕ) => ‖∫ (x : ℝ), (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial) * ↑↑f x ∂ProbabilityTheory.gaussianReal 0 1‖ ^ 2

The squared norms of the Gaussian Hermite coefficients of an L² function are summable.

theorem TauCeti.hasSum_gaussianHermite_expansion {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))) : HasSum (fun (n : ℕ) => (∫ (x : ℝ), (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial) * ↑↑f x ∂ProbabilityTheory.gaussianReal 0 1) • (gaussianHermiteHilbertBasis 𝕜) n) f

The Gaussian Hermite expansion. Every f ∈ L²(N(0, 1); 𝕜) is the sum of its normalized Hermite-polynomial series.