The Hermite functions as a Hilbert basis of L²(ℝ)

This file instantiates the weighted-measure machinery at the Gaussian weight w(x) = e^{-x²} and the dilated Hermite polynomials Hₙ(x√2), whose √w-envelope is exactly the Hermite function ψₙ of TauCeti.hermiteFunction.

Main statements

• TauCeti.degree_hermiteDilated — Hₙ(x√2) has degree exactly n.
• TauCeti.integral_hermiteDilated_mul_hermiteDilated_mul_gaussianWeight — the orthogonality relation with normalization cₙ = n!√π, obtained from the Hermite function orthonormality (milestone A2).
• TauCeti.hermiteHilbertBasis — milestone A3: the Hermite functions as a HilbertBasis of L²(ℝ), the principal result of this file.
• TauCeti.coe_hermiteHilbertBasis — its normal form: the n-th basis vector really is ψₙ.

theorem TauCeti.degree_hermiteDilated (n : ℕ) : (hermiteDilated n).degree = ↑n

The dilation preserves degrees: Hₙ(√2 · X) has degree exactly n.

TauCeti.hermiteDilated itself lives in the MemLp layer, where the membership results are already stated about it; only this degree fact is new here, and only the basis construction needs it.

theorem TauCeti.hermiteNormalization_pos (n : ℕ) : 0 < ↑n.factorial * √Real.pi

The Hermite normalization cₙ = n!·√π is positive.

theorem TauCeti.integral_hermiteDilated_mul_hermiteDilated_mul_gaussianWeight (m n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (hermiteDilated m) * Polynomial.eval x (hermiteDilated n) * Real.exp (-x ^ 2) = if m = n then ↑n.factorial * √Real.pi else 0

Orthogonality against the Gaussian weight. ∫ Hₘ(x√2)Hₙ(x√2)e^{-x²} = δₘₙ·n!√π. This is the Hermite function orthonormality (milestone A2) with the normalizations put back.

noncomputable def TauCeti.hermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)

Roadmap A3: the Hermite functions are a Hilbert basis of L²(ℝ). Orthonormality comes from the weighted-measure machinery and completeness from moment determinacy (TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot), applied to the exact-degree family Hₙ(x√2) against the Gaussian weight e^{-x²}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_hermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : ⇑(hermiteHilbertBasis 𝕜) = hermiteFunctionLp 𝕜

The basis vectors are the Hermite functions. Without this the construction would only exhibit some Hilbert basis; here the √w-envelope of Hₙ(x√2)/√cₙ is identified with ψₙ.