L² membership of the Hermite polynomials against a Gaussian measure

This file specializes the generic Gaussian/polynomial L² membership of TauCeti.Probability.Distributions.Gaussian.PolynomialMemLp to the probabilists' Hermite polynomials Polynomial.hermite n. The Hermite statement memLp_hermite_gaussianReal is target A3′ of the OrthogonalL2Bases roadmap: the variance-general L² membership of the normalized Hermite polynomials Hₙ / √(n!) under gaussianReal 0 v, the membership the Gaussian Hermite Hilbert-basis construction consumes for its MemLp obligations.

The scalar-generic cast to [RCLike 𝕜] (needed because the roadmap's bases are stated over Lp 𝕜 2 μ uniformly for 𝕜 = ℝ and 𝕜 = ℂ) reuses Mathlib's MemLp.ofReal, rewriting the algebraMap ℝ 𝕜 cast to RCLike.ofReal.

The Polynomial evaluation API and MemLp.ofReal are consumed, not re-derived.

Scalar-generic cast and the Hermite instance

theorem TauCeti.memLp_hermite_gaussianReal {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) (v : NNReal) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial)) 2 (ProbabilityTheory.gaussianReal 0 v)

Target A3′ (variance-general L² membership). The normalized probabilists' Hermite polynomial Hₙ / √(n!), cast into 𝕜, is square-integrable against every centred real Gaussian gaussianReal 0 v. Immediate from memLp_two_eval_gaussianReal (Hermite is a polynomial) and the scalar cast MemLp.ofReal.