Orthonormality of the Hermite functions

This file proves that the Hermite functions ψₙ(x) = Hₙ(x√2) exp(-x²/2) / √(n!√π) (TauCeti.hermiteFunction) form an orthonormal system in L²(ℝ), the roadmap milestones A2 (pointwise) and A3 (the Lp orthonormality the hermiteHilbertBasis construction consumes) of TauCetiRoadmap/OrthogonalL2Bases/README.md.

• TauCeti.integral_hermiteFunction_mul_hermiteFunction: ∫ x, ψₘ(x) · ψₙ(x) = if m = n then 1 else 0, the pointwise orthonormality relation. It is the polynomial orthogonality relation TauCeti.integral_hermite_mul_hermite_mul_gaussian (∫ Hₘ Hₙ e^{-x²/2} = if m = n then n!√(2π) else 0, milestone A1) transported across the dilation u = x√2 (MeasureTheory.Measure.integral_comp_mul_right): the Gaussian envelope exp(-x²/2)² collapses to exp(-(x√2)²/2), and the normalizations √(n!√π) cancel the n!√(2π) self-pairing up to the Jacobian (√2)⁻¹.
• TauCeti.inner_hermiteFunctionLp: ⟪ψₘ, ψₙ⟫ = if m = n then 1 else 0 for the Lp 𝕜 2 volume vectors, over any RCLike scalar field 𝕜, obtained by rewriting the L² inner product as the pointwise integral above.
• TauCeti.orthonormal_hermiteFunctionLp: Orthonormal 𝕜 (hermiteFunctionLp 𝕜), immediate from the inner-product formula via orthonormal_iff_ite.
• TauCeti.norm_hermiteFunctionLp: every Hermite mode has L² norm one.

The lower-level zeroth-mode normalizations TauCeti.integral_hermiteFunction_zero_mul_self and TauCeti.norm_hermiteFunctionLp_zero remain available to importers that do not need the full orthonormality development; TauCeti.norm_hermiteFunctionLp 0 is the general theorem specialized to that mode.

Pointwise orthonormality

theorem TauCeti.integral_hermiteFunction_mul_hermiteFunction (m n : ℕ) : ∫ (x : ℝ), hermiteFunction m x * hermiteFunction n x = if m = n then 1 else 0

Target A2 (orthonormality). The Hermite functions are pointwise orthonormal in L²(ℝ): ∫ x, ψₘ(x) · ψₙ(x) = if m = n then 1 else 0. This is the polynomial orthogonality relation integral_hermite_mul_hermite_mul_gaussian pushed through the dilation u = x√2.

Orthonormality of the Lp Hermite vectors

theorem TauCeti.inner_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] (m n : ℕ) : inner 𝕜 (hermiteFunctionLp 𝕜 m) (hermiteFunctionLp 𝕜 n) = if m = n then 1 else 0

Target A3 (orthonormality, inner-product form). The Lp Hermite vectors satisfy ⟪ψₘ, ψₙ⟫ = if m = n then 1 else 0, over any RCLike scalar field, by evaluating the L² inner product as the pointwise integral integral_hermiteFunction_mul_hermiteFunction.

theorem TauCeti.orthonormal_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] : Orthonormal 𝕜 (hermiteFunctionLp 𝕜)

Target A3 (orthonormality). The Lp Hermite functions form an orthonormal system in L²(ℝ; 𝕜), for any RCLike scalar field 𝕜. This is the orthonormality input the hermiteHilbertBasis construction feeds to HilbertBasis.mkOfOrthogonalEqBot.

@[simp]

theorem TauCeti.norm_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) : ‖hermiteFunctionLp 𝕜 n‖ = 1

Target A2 (unit norm). Every Hermite function has L² norm one, over any RCLike scalar field.