The multi-index Hermite basis of a multivariate Gaussian L²

The Fintype-indexed product of the one-dimensional Gaussian Hermite basis: the multi-index family Ψ_a(x) = ∏ᵢ H_{aᵢ}(xᵢ)/√(aᵢ!) is a Hilbert basis of L²(γ^ι), the standard basis for multivariate Gaussian L² and for chaos expansions.

Both inputs are already in place, so the basis itself is a combination: TauCeti.piHilbertBasis builds a Hilbert basis of L²(Measure.pi μ) from coordinatewise bases, and TauCeti.gaussianHermiteHilbertBasis is the one-dimensional factor.

The file then relates this measure-side basis to the function-side multi-index Hermite-function basis TauCeti.hermiteFunctionPiBasis of L²(volume^ι). As in one dimension (TauCeti.weightL2Isometry_gaussianHermiteHilbertBasis), the two are not interchanged by the weight-to-function isometry alone: because ψₙ is built on the rescaled argument x√2, the image of Ψ_a under TauCeti.weightL2Isometry for the joint Gaussian density is the dilated product ∏ᵢ 2^{-1/4} ψ_{aᵢ}(xᵢ/√2). The dilation and the 2^{-1/4} appear once per coordinate, which is exactly the statement the roadmap asks for.

Main statements

• TauCeti.gaussianHermitePiBasis — the multi-index basis.
• TauCeti.gaussianHermitePiBasis_apply — the a-th vector is the tensor TauCeti.L2piMul of the one-dimensional Gaussian Hermite vectors, as an equality of L² vectors.
• TauCeti.coeFn_gaussianHermitePiBasis — the anti-vacuity pin: the a-th vector really is the product ∏ᵢ H_{aᵢ}(xᵢ)/√(aᵢ!).
• TauCeti.sqrt_prod_gaussianPDFReal_smul_gaussianHermitePiBasis: scaling the a-th vector by the square root of the joint Gaussian density gives ∏ᵢ 2^{-1/4} ψ_{aᵢ}(xᵢ/√2).
• TauCeti.weightL2Isometry_gaussianHermitePiBasis: the same identification at the TauCeti.weightL2Isometry level.

noncomputable def TauCeti.gaussianHermitePiBasis (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] : HilbertBasis (ι → ℕ) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))

The multivariate Gaussian Hermite basis. piHilbertBasis over the one-dimensional Gaussian Hermite basis in every coordinate.

Equations

• TauCeti.gaussianHermitePiBasis 𝕜 ι = TauCeti.piHilbertBasis fun (x : ι) => TauCeti.gaussianHermiteHilbertBasis 𝕜

@[simp]

theorem TauCeti.gaussianHermitePiBasis_apply (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] (a : ι → ℕ) : (gaussianHermitePiBasis 𝕜 ι) a = L2piMul fun (i : ι) => (gaussianHermiteHilbertBasis 𝕜) (a i)

The a-th basis vector is the tensor of the one-dimensional Gaussian Hermite vectors. Stated between L² vectors, this is what the expansion API rewrites with, since the inner product against a tensor factors coordinatewise (TauCeti.inner_L2piMul); TauCeti.coeFn_gaussianHermitePiBasis below refines it to a pointwise product of polynomials.

theorem TauCeti.coeFn_gaussianHermitePiBasis (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] (a : ι → ℕ) : ↑↑((gaussianHermitePiBasis 𝕜 ι) a) =ᵐ[MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1] fun (x : ι → ℝ) => ∏ i : ι, (algebraMap ℝ 𝕜) ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)

The basis vectors are the multi-index Hermite products. Without this the construction would only exhibit some Hilbert basis of L²(γ^ι). The coordinatewise identification transfers to the product measure because each evaluation map pushes the product's a.e. filter into the factor's (MeasureTheory.Measure.tendsto_eval_ae_ae).

theorem TauCeti.sqrt_prod_gaussianPDFReal_smul_gaussianHermitePiBasis (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] (a : ι → ℕ) : (fun (x : ι → ℝ) => √(∏ i : ι, ProbabilityTheory.gaussianPDFReal 0 1 (x i)) • ↑↑((gaussianHermitePiBasis 𝕜 ι) a) x) =ᵐ[MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume] fun (x : ι → ℝ) => ∏ i : ι, (algebraMap ℝ 𝕜) ((√√2)⁻¹ * hermiteFunction (a i) (x i / √2))

The joint Gaussian envelope of a multi-index basis vector is a dilated Hermite-function product. Scaling the a-th vector of L²(γ^ι) by the square root of the joint density gives ∏ᵢ 2^{-1/4} ψ_{aᵢ}(xᵢ/√2), with 2^{-1/4} written as (√√2)⁻¹ to stay inside Real.sqrt.

Stated volume^ι-almost everywhere, the measure the envelope lives on; the move from γ^ι-almost everywhere is legitimate because the joint density never vanishes (TauCeti.Probability.pi_volume_absolutelyContinuous_pi_gaussianReal). Every coordinate contributes one factor of the one-dimensional identity TauCeti.sqrt_gaussianPDFReal_mul_hermiteℝ_div_sqrt_factorial, so the dilation xᵢ ↦ xᵢ/√2 really is coordinatewise.

theorem TauCeti.weightL2Isometry_gaussianHermitePiBasis (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] (a : ι → ℕ) : ↑↑((weightL2Isometry (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume) (fun (x : ι → ℝ) => ∏ i : ι, ProbabilityTheory.gaussianPDFReal 0 1 (x i)) ⋯ ⋯) (cast ⋯ ((gaussianHermitePiBasis 𝕜 ι) a))) =ᵐ[MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume] fun (x : ι → ℝ) => ∏ i : ι, (algebraMap ℝ 𝕜) ((√√2)⁻¹ * hermiteFunction (a i) (x i / √2))

The TauCeti.weightL2Isometry-image of the multi-index Gaussian Hermite basis is the dilated multi-index Hermite-function family. The a-th vector goes to ∏ᵢ 2^{-1/4} • ψ_{aᵢ}(xᵢ/√2), pinning the measure-side basis of L²(γ^ι) to the function-side TauCeti.hermiteFunctionPiBasis of L²(volume^ι) up to that coordinatewise dilation and normalization.

TauCeti.weightL2Isometry has L²((volume^ι).withDensity …) as its domain, whereas TauCeti.gaussianHermitePiBasis lives in the propositionally equal L²(γ^ι), so the basis vector is transported along TauCeti.Probability.pi_gaussianReal_eq_withDensity before the isometry is applied. The positivity and measurability of the joint density are supplied here rather than left to the caller; by proof irrelevance the statement still applies to TauCeti.weightL2Isometry built from any other proofs of those two side conditions.