Integrability and L² membership of polynomials against a Gaussian measure

This file collects the family-agnostic facts that a real polynomial, evaluated pointwise, is integrable and square-integrable against a real Gaussian measure gaussianReal μ v, together with the companion statement that a polynomial times a Gaussian envelope exp (-(x - μ)²/(2v)) is Lebesgue-integrable and that a Gaussian weight has finite exponential moments. These hold for any q : ℝ[X] and feed the Hermite-specific L² membership in TauCeti.Probability.Distributions.Gaussian.Hermite.MemLp and the Hermite-function integrability in TauCeti.Analysis.SpecialFunctions.Hermite.Function.MemLp.

The L² argument factors through the family-agnostic memLp_two_eval_of_forall_integrable_pow (TauCeti.MeasureTheory.Function.PolynomialMemLp), which holds for any reference measure on ℝ all of whose polynomial moments are finite. The Gaussian instance supplies that moment hypothesis ∀ k, Integrable (x ↦ xᵏ) from Mathlib's memLp_id_gaussianReal' (all moments of a real Gaussian are finite). The envelope statement transports the polynomial's integrability against the Gaussian measure across gaussianReal μ v = volume.withDensity (gaussianPDF μ v).

Mathlib's memLp_id_gaussianReal' (Fernique) and Gaussian density API (gaussianReal_of_var_ne_zero, measurable_gaussianPDF, gaussianPDFReal_def) are consumed, not re-derived.

Exponential moments of Gaussian weights

theorem TauCeti.integrable_exp_mul_abs_gaussianWeight {b : ℝ} (hb : 0 < b) (a : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (Real.exp (-(b * x ^ 2))))

Finite exponential moments of a Gaussian weight. For every rate a and every width b > 0, the function e^{a|x|} is integrable against e^{-bx²}·dx, because a|x| ≤ a²/(2b) + bx²/2 gives the domination e^{a|x|}e^{-bx²} ≤ e^{a²/(2b)}·e^{-bx²/2}.

The Gaussian instance

theorem TauCeti.integrable_pow_gaussianReal (μ : ℝ) (v : NNReal) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (ProbabilityTheory.gaussianReal μ v)

Every polynomial moment of a real Gaussian measure is finite: x ↦ xⁿ is integrable against gaussianReal μ v. This is memLp_id_gaussianReal' (all moments finite) unwound to plain integrability of the power.

theorem TauCeti.memLp_two_eval_gaussianReal (μ : ℝ) (v : NNReal) (q : Polynomial ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => Polynomial.eval x q) 2 (ProbabilityTheory.gaussianReal μ v)

A real polynomial is square-integrable against every real Gaussian measure.

Polynomial times a Gaussian envelope

theorem TauCeti.integrable_eval_mul_gaussianEnvelope (μ : ℝ) (q : Polynomial ℝ) {w : NNReal} (hw : w ≠ 0) : MeasureTheory.Integrable (fun (x : ℝ) => Polynomial.eval x q * Real.exp (-(x - μ) ^ 2 / (2 * ↑w))) MeasureTheory.volume

A real polynomial evaluated pointwise, times a Gaussian envelope exp (-(x - μ)²/(2v)) of positive variance v centered at μ, is Lebesgue-integrable. Transported from the polynomial's integrability against the Gaussian measure gaussianReal μ v across gaussianReal μ v = volume.withDensity (gaussianPDF μ v).

theorem TauCeti.integrable_eval_mul_exp_neg_sq (q : Polynomial ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Polynomial.eval x q * Real.exp (-x ^ 2)) MeasureTheory.volume

A real polynomial times the envelope exp(-x²) is Lebesgue-integrable — the centered v = ½ case of integrable_eval_mul_gaussianEnvelope.