The Hermite polynomials as a Hilbert basis of L²(γ)

Roadmap milestone A3′: the measure-side one-dimensional Gaussian Hermite basis. Where TauCeti.hermiteHilbertBasis puts the Gaussian envelope inside the function (ψₙ in L²(ℝ)), this puts it in the measure: Hₙ/√(n!) is an orthonormal basis of L²(γ) for the standard Gaussian γ = gaussianReal 0 1.

That is the form multivariate Gaussian L² and chaos expansions consume, and it is the input piHilbertBasis needs for the multidimensional basis of Part D.

Main statements

• TauCeti.integral_hermite_mul_hermite_mul_gaussianPDFReal — the orthogonality relation against the standard Gaussian density, with normalization cₙ = n!.
• TauCeti.integrable_exp_mul_abs_gaussianPDFReal — the standard Gaussian density has every exponential moment finite, the hypothesis TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot needs.
• TauCeti.gaussianHermiteHilbertBasis — milestone A3′ itself.
• TauCeti.coeFn_gaussianHermiteHilbertBasis — the anti-vacuity pin: the basis vectors really are Hₙ/√(n!), not merely some orthonormal basis.
• TauCeti.sqrt_gaussianPDFReal_mul_hermiteℝ_div_sqrt_factorial — the √w-envelope of a basis vector is 2^{-1/4}·ψₙ(x/√2), identifying this basis with the function-side TauCeti.hermiteHilbertBasis through TauCeti.weightL2Isometry.
• TauCeti.sqrt_gaussianPDFReal_smul_gaussianHermiteHilbertBasis — that envelope computed on the public basis vector itself, a.e. against volume.
• TauCeti.weightL2Isometry_gaussianHermiteHilbertBasis — the same identification at the TauCeti.weightL2Isometry level: the image of the n-th basis vector is 2^{-1/4} • ψₙ(·/√2).

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

Orthogonality against the standard Gaussian density. ∫ Hₘ Hₙ dγ = δₘₙ · n!. This is the density-side reading of the Gaussian-measure orthogonality milestone TauCeti.integral_hermite_mul_hermite_gaussianReal: ∫ · ∂γ unfolds to ∫ pdf • ·, so the two differ only by the order of the factors.

The weighted-measure input data

TauCeti.hermiteℝ and its eval/degree lemmas live in TauCeti/RingTheory/Polynomial/Hermite/Real.lean: they mention no measure and no Gaussian, and keeping them here would strand them below the function-side files that use the same cast.

theorem TauCeti.integrable_exp_mul_abs_gaussianPDFReal (a : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 1 x))

Finite exponential moments of the standard Gaussian. For every rate a, e^{a|x|} is integrable against γ.

Both one-sided exponentials are already integrable against a Gaussian (ProbabilityTheory.integrable_exp_mul_gaussianReal, which is the mgf being everywhere finite), and ProbabilityTheory.integrable_exp_mul_abs folds the rates a and -a into the two-sided e^{a|x|}. Transporting along ProbabilityTheory.gaussianReal_of_var_ne_zero then puts it in the with-density form the completeness theorem takes; the ENNReal.ofReal ∘ gaussianPDFReal spelling of the density is definitionally the gaussianPDF that lemma produces.

theorem TauCeti.exp_moment_gaussianPDFReal : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 1 x))

The exponential-moment hypothesis in the existential form the completeness theorem takes.

noncomputable def TauCeti.gaussianHermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))

Roadmap A3′: the Hermite polynomials are a Hilbert basis of L²(γ). Orthonormality comes from the orthogonality relation against the Gaussian density and completeness from moment determinacy (TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot), applied to the exact-degree family Hₙ. Where TauCeti.hermiteHilbertBasis carries the Gaussian in the function, this carries it in the measure — the form multivariate L²(γ^ι) and chaos expansions consume.

Equations

• TauCeti.gaussianHermiteHilbertBasis 𝕜 = cast ⋯ (TauCeti.gaussianHermiteHilbertBasisAux✝ 𝕜)

theorem TauCeti.coeFn_gaussianHermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↑↑((gaussianHermiteHilbertBasis 𝕜) n) =ᵐ[ProbabilityTheory.gaussianReal 0 1] fun (x : ℝ) => (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial)

The basis vectors are the normalized Hermite polynomials. Without this the construction would only exhibit some Hilbert basis of L²(γ); here each vector is pinned to Hₙ/√(n!), which is what downstream chaos-coordinate computations need.

theorem TauCeti.sqrt_gaussianPDFReal_mul_hermiteℝ_div_sqrt_factorial (n : ℕ) (x : ℝ) : √(ProbabilityTheory.gaussianPDFReal 0 1 x) * (Polynomial.eval x (hermiteℝ n) / √↑n.factorial) = (√√2)⁻¹ * hermiteFunction n (x / √2)

The Gaussian envelope carries Hₙ/√(n!) to a dilated Hermite function. √(γ-density x) · Hₙ(x)/√(n!) = 2^{-1/4} · ψₙ(x/√2), with 2^{-1/4} written as (√√2)⁻¹ to stay inside Real.sqrt.

Multiplication by √w is exactly TauCeti.weightL2Isometry, so this is the pointwise characterization of that isometry's image on TauCeti.gaussianHermiteHilbertBasis: it pins the measure-side basis of L²(γ) to the function-side basis TauCeti.hermiteHilbertBasis of L²(ℝ), up to the dilation x ↦ x/√2 and that normalization. Without it a consumer moving between the two normalizations has to redo the dilation and normalization bookkeeping.

theorem TauCeti.sqrt_gaussianPDFReal_smul_gaussianHermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : (fun (x : ℝ) => √(ProbabilityTheory.gaussianPDFReal 0 1 x) • ↑↑((gaussianHermiteHilbertBasis 𝕜) n) x) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => (√√2)⁻¹ • (algebraMap ℝ 𝕜) (hermiteFunction n (x / √2))

The Gaussian envelope of the basis is the dilated Hermite function family. Scaling the n-th basis vector of L²(γ) by √(γ-density) gives 2^{-1/4} • ψₙ(·/√2).

Stated a.e. against volume, the measure that envelope lives on, and in terms of the public gaussianHermiteHilbertBasis rather than its weighted-measure preimage. The pointwise content is TauCeti.sqrt_gaussianPDFReal_mul_hermiteℝ_div_sqrt_factorial; the only work here is moving the basis representative from γ-a.e. to volume-a.e., which is legitimate because the Gaussian density never vanishes.

√w-scaling is the forward map of TauCeti.weightL2Isometry, so this is the pointwise content of TauCeti.weightL2Isometry_gaussianHermiteHilbertBasis below, which states the same fact at the isometry level.

theorem TauCeti.weightL2Isometry_gaussianHermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↑↑((weightL2Isometry MeasureTheory.volume (fun (x : ℝ) => ProbabilityTheory.gaussianPDFReal 0 1 x) ⋯ weightL2Isometry_gaussianHermiteHilbertBasis._proof_1) (cast ⋯ ((gaussianHermiteHilbertBasis 𝕜) n))) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => (√√2)⁻¹ • (algebraMap ℝ 𝕜) (hermiteFunction n (x / √2))

The weightL2Isometry-image of the Gaussian Hermite basis is the dilated Hermite function family. The n-th vector goes to 2^{-1/4} • ψₙ(·/√2), pinning the measure-side basis of L²(γ) to the function-side basis TauCeti.hermiteHilbertBasis of L²(ℝ) up to that dilation and normalization.

TauCeti.weightL2Isometry has L²(volume.withDensity …) as its domain, whereas TauCeti.gaussianHermiteHilbertBasis lives in the propositionally equal L²(γ), so the basis vector is transported along that equality of measures before the isometry is applied. The weight is the fixed function gaussianPDFReal 0 1, whose positivity and measurability are supplied here rather than left to the caller; by proof irrelevance this still applies to TauCeti.weightL2Isometry built from any other proofs of those two side conditions.