Integrability, L² membership, and normalization of the Hermite functions

This file continues the object API for the Hermite functions ψₙ(x) = Hₙ(x√2) exp(-x²/2) / √(n!√π) (TauCeti.hermiteFunction), adding the regularity facts the OrthogonalL2Bases roadmap's A2 milestone lists and its A3 basis construction consumes:

• TauCeti.integrable_hermiteFunction — every ψₙ is integrable against Lebesgue measure;
• TauCeti.memLp_two_hermiteFunction — every ψₙ is in L²(volume), the membership the hermiteFunctionLp/hermiteHilbertBasis layer needs to package ψₙ as an Lp element.
• TauCeti.integral_hermiteFunction_zero_mul_self — the zeroth Hermite function has square integral one.

The membership results use the reusable engine TauCeti.integrable_eval_mul_gaussianEnvelope: a real polynomial evaluated pointwise, times a Gaussian envelope exp(-(x - μ)²/(2v)) of any center μ and positive variance v, is Lebesgue-integrable. It is obtained by transporting the polynomial's integrability against the Gaussian measure gaussianReal μ v (all of whose moments are finite, TauCeti.integrable_pow_gaussianReal, so TauCeti.integrable_eval_of_forall_integrable_pow applies) across the change of variables gaussianReal μ v = volume.withDensity (gaussianPDF μ v) with integrable_withDensity_iff. Applied to the polynomial Hₙ(·√2) with v = 1 this gives the L¹ membership, and to its square with v = ½ (whose envelope exp(-x²) is ψₙ² up to the constant) the L² membership. The zeroth-mode normalization additionally uses Mathlib's Gaussian density normalization integral_gaussianPDFReal_eq_one.

Mathlib's Gaussian density API (gaussianReal_of_var_ne_zero, measurable_gaussianPDF, gaussianPDFReal_def), integrable_withDensity_iff, memLp_two_iff_integrable_sq, and the Polynomial evaluation API are consumed, not re-derived.

L¹ and L² membership of the Hermite functions

noncomputable def TauCeti.hermiteDilated (n : ℕ) : Polynomial ℝ

The dilated Hermite polynomial Hₙ(√2 · X), the polynomial whose Gaussian envelope is the Hermite function ψₙ.

It is defined at this layer rather than at the basis layer because every MemLp result below is already about it: ψₙ is this polynomial times exp(-x²/2), up to normalization.

Equations

• TauCeti.hermiteDilated n = (TauCeti.hermiteℝ n).comp (Polynomial.C √2 * Polynomial.X)

theorem TauCeti.hermiteDilated_def (n : ℕ) : hermiteDilated n = (hermiteℝ n).comp (Polynomial.C √2 * Polynomial.X)

The defining equation of TauCeti.hermiteDilated, exported so that consumers in other modules can rewrite with it.

theorem TauCeti.eval_hermiteDilated (n : ℕ) (x : ℝ) : Polynomial.eval x (hermiteDilated n) = (Polynomial.aeval (x * √2)) (Polynomial.hermite n)

Evaluating the dilated Hermite polynomial is aeval (·√2).

theorem TauCeti.integrable_hermiteFunction (n : ℕ) : MeasureTheory.Integrable (hermiteFunction n) MeasureTheory.volume

Target A2 (L¹). Each Hermite function is integrable against Lebesgue measure: it is a polynomial in x times the Gaussian envelope exp(-x²/2), the v = 1 case of integrable_eval_mul_gaussianEnvelope.

theorem TauCeti.memLp_two_hermiteFunction (n : ℕ) : MeasureTheory.MemLp (hermiteFunction n) 2 MeasureTheory.volume

Target A2 (L²). Each Hermite function lies in L²(volume). Its square is (Hₙ(x√2))² exp(-x²) up to the constant (n!√π), integrable by integrable_eval_mul_exp_neg_sq, and L² membership is integrability of the square (memLp_two_iff_integrable_sq). This is the membership hermiteFunctionLp needs to realize ψₙ as an element of Lp ℝ 2 volume.

Zeroth-mode normalization

theorem TauCeti.integral_hermiteFunction_zero_mul_self : ∫ (x : ℝ), hermiteFunction 0 x * hermiteFunction 0 x = 1

The zeroth Hermite function has square integral one. This is the n = 0 boundary case of the roadmap's Hermite-function orthonormality target.