The Gaussian orthogonality relation for the probabilists' Hermite polynomials

Mathlib defines the probabilists' Hermite polynomials Polynomial.hermite : ℕ → ℤ[X] and knows the Gaussian integral ∫ x, exp (-b x²) = √(π / b), but it records no orthogonality relation between the Hermite polynomials against the Gaussian weight. This file proves that relation, the milestone A1 of the OrthogonalL2Bases roadmap (TauCetiRoadmap/OrthogonalL2Bases/README.md, Part A1): the Hermite polynomials are pairwise orthogonal, and self-paired to n! · √(2π), in L² of the Gaussian weight.

• integrable_aeval_mul_gaussian: every polynomial is integrable against the Gaussian weight e^{-x²/2};
• integral_aeval_mul_hermite_succ, the one-step weighted-pairing recursion ∫ p · H_{n+1} · w = ∫ p' · Hₙ · w;
• integral_aeval_mul_hermite, iterating the recursion, ∫ p · Hₙ · w = ∫ (dⁿ/dxⁿ p) · w;
• Milestone (Lebesgue form) integral_hermite_mul_hermite_mul_gaussian: ∫ x, Hₘ(x) · Hₙ(x) · e^{-x²/2} = if m = n then n! · √(2π) else 0, obtained by peeling the larger index down to a constant (Polynomial.iterate_derivative_hermite);
• Milestone (Gaussian-measure form) integral_hermite_mul_hermite_gaussianReal: ∫ x, Hₘ(x) · Hₙ(x) ∂(gaussianReal 0 1) = if m = n then n! else 0, the Lebesgue form divided by the √(2π) density. This is the form the Gaussian Hermite basis (A3′) consumes directly.

The closed form of the density itself, gaussianPDFReal 0 1 x = (√(2π))⁻¹ · e^{-x²/2}, is a fact about the Gaussian distribution rather than about the Hermite family, and lives in TauCeti.Probability.Distributions.Gaussian.Basic as TauCeti.Probability.gaussianPDFReal_zero_one.

The Hermite lowering identities Polynomial.derivative_hermite, Polynomial.iterate_derivative_hermite are reused from TauCeti/RingTheory/Polynomial/Hermite/Derivative.lean.

theorem TauCeti.integrable_aeval_mul_gaussian (p : Polynomial ℤ) : MeasureTheory.Integrable (fun (x : ℝ) => (Polynomial.aeval x) p * Real.exp (-(x ^ 2 / 2))) MeasureTheory.volume

Integrability of a polynomial against the Gaussian weight e^{-x²/2}: every real polynomial, evaluated pointwise and multiplied by the Gaussian weight, is Lebesgue-integrable.

theorem TauCeti.integral_aeval_mul_hermite_succ (p : Polynomial ℤ) (n : ℕ) : ∫ (x : ℝ), (Polynomial.aeval x) p * (Polynomial.aeval x) (Polynomial.hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)) = ∫ (x : ℝ), (Polynomial.aeval x) (Polynomial.derivative p) * (Polynomial.aeval x) (Polynomial.hermite n) * Real.exp (-(x ^ 2 / 2))

One-step weighted-pairing recursion (target A1): the weighted pairing of p with H_{n+1} equals the weighted pairing of its derivative p' with Hₙ, ∫ p · H_{n+1} · e^{-x²/2} = ∫ p' · Hₙ · e^{-x²/2}.

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

The Hermite orthogonality relation, Lebesgue form (milestone A1): ∫ x, Hₘ(x) · Hₙ(x) · e^{-x²/2} = if m = n then n! · √(2π) else 0.

theorem TauCeti.integral_hermite_mul_hermite_gaussianReal (m n : ℕ) : ∫ (x : ℝ), (Polynomial.aeval x) (Polynomial.hermite m) * (Polynomial.aeval x) (Polynomial.hermite n) ∂ProbabilityTheory.gaussianReal 0 1 = if m = n then ↑n.factorial else 0

The Hermite orthogonality relation, Gaussian-measure form (milestone A1): ∫ x, Hₘ(x) · Hₙ(x) ∂(gaussianReal 0 1) = if m = n then n! else 0. This is the Lebesgue form divided by the √(2π) density; it is the relation the Gaussian Hermite basis (A3′) consumes.