Parseval and expansions for the multivariate Gaussian Hermite basis

TauCeti.gaussianHermitePiBasis exhibits the multi-index Hermite products Ψ_a(x) = ∏ᵢ H_{aᵢ}(xᵢ)/√(aᵢ!) as a Hilbert basis of L²(γ^ι), γ = N(0, 1). This file supplies the coefficient, Parseval, and reconstruction API for that basis: the expansion of an L² function of ι independent standard Gaussians into multivariate Hermite polynomials, the finite-dimensional form of a chaos expansion. It is the Fintype-indexed analogue of TauCeti.hasSum_gaussianHermite_expansion and its neighbours.

As in one dimension the coefficient has no name of its own: it is spelled out as the integral against ∏ᵢ H_{aᵢ}/√(aᵢ!), and the Parseval-side lemmas are named after that integral.

At this arity the file additionally gives the coordinate as an integral, proves that its integrand is integrable, and specializes TauCeti.piHilbertBasis_repr_L2piMul to factor the coordinates of a product function into the one-dimensional coordinates of its factors.

Main statements

• TauCeti.gaussianHermitePiBasis_repr_apply identifies each coordinate with its integral, whose integrand is integrable by TauCeti.integrable_prod_hermite_div_sqrt_factorial_mul_pi_gaussianReal.
• TauCeti.gaussianHermitePiBasis_repr_L2piMul factors the coordinates of a product function.
• TauCeti.tsum_inner_mul_inner_L2piMul_gaussianHermiteHilbertBasis is Parseval in polarized form.
• TauCeti.tsum_norm_sq_integral_prod_hermite_mul_pi_gaussianReal is Parseval's identity for those coefficients.
• TauCeti.summable_norm_sq_integral_prod_hermite_mul_pi_gaussianReal gives square-summability of the coefficients.
• TauCeti.hasSum_gaussianHermitePi_expansion reconstructs every L²(γ^ι) vector from its multivariate Hermite series.

All statements hold for an arbitrary RCLike scalar field, simultaneously covering real and complex-valued L² functions.

theorem TauCeti.integrable_prod_hermite_div_sqrt_factorial_mul_pi_gaussianReal {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))) (a : ι → ℕ) : MeasureTheory.Integrable (fun (x : ι → ℝ) => (∏ i : ι, (algebraMap ℝ 𝕜) ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)) * ↑↑f x) (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1)

The integrand of the coordinate integral below is integrable: it is the pointwise inner product of two L² functions.

theorem TauCeti.gaussianHermitePiBasis_repr_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))) (a : ι → ℕ) : ↑((gaussianHermitePiBasis 𝕜 ι).repr f) a = ∫ (x : ι → ℝ), (∏ i : ι, (algebraMap ℝ 𝕜) ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)) * ↑↑f x ∂MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1

The a-th multivariate Gaussian Hermite coordinate of f is the integral of f against the normalized multi-index Hermite product ∏ᵢ H_{aᵢ}(xᵢ)/√(aᵢ!). The polynomials are real, so no complex conjugate survives.

@[simp]

theorem TauCeti.gaussianHermitePiBasis_repr_L2piMul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (F : ι → ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))) (a : ι → ℕ) : ↑((gaussianHermitePiBasis 𝕜 ι).repr (L2piMul F)) a = ∏ i : ι, ∫ (x : ℝ), (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite (a i)) / √↑(a i).factorial) * ↑↑(F i) x ∂ProbabilityTheory.gaussianReal 0 1

The multi-index coordinates of a product function factor. If f(x) = ∏ᵢ Fᵢ(xᵢ) for one-dimensional L²(N(0, 1)) factors Fᵢ, its a-th multivariate Hermite coordinate is the product of the aᵢ-th one-dimensional Hermite coordinates of the factors: a multivariate chaos expansion of a product of independent variables is computable from one-dimensional ones.

theorem TauCeti.tsum_inner_mul_inner_L2piMul_gaussianHermiteHilbertBasis {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f g : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))) : ∑' (a : ι → ℕ), inner 𝕜 f (L2piMul fun (i : ι) => (gaussianHermiteHilbertBasis 𝕜) (a i)) * inner 𝕜 (L2piMul fun (i : ι) => (gaussianHermiteHilbertBasis 𝕜) (a i)) g = inner 𝕜 f g

Parseval's identity for the multivariate Gaussian Hermite basis (polarized form): the multi-index Gaussian Hermite coordinates of f and g pair to their inner product.

theorem TauCeti.tsum_norm_sq_integral_prod_hermite_mul_pi_gaussianReal {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))) : ∑' (a : ι → ℕ), ‖∫ (x : ι → ℝ), (∏ i : ι, (algebraMap ℝ 𝕜) ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)) * ↑↑f x ∂MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the multivariate Gaussian Hermite basis. The squared coefficients of f against the multi-index Hermite products sum to ‖f‖².

theorem TauCeti.summable_norm_sq_integral_prod_hermite_mul_pi_gaussianReal {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))) : Summable fun (a : ι → ℕ) => ‖∫ (x : ι → ℝ), (∏ i : ι, (algebraMap ℝ 𝕜) ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)) * ↑↑f x ∂MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1‖ ^ 2

The squared multivariate Gaussian Hermite coefficients of an L²(γ^ι) function are summable.

theorem TauCeti.hasSum_gaussianHermitePi_expansion {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1))) : HasSum (fun (a : ι → ℕ) => (∫ (x : ι → ℝ), (∏ i : ι, (algebraMap ℝ 𝕜) ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)) * ↑↑f x ∂MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1) • L2piMul fun (i : ι) => (gaussianHermiteHilbertBasis 𝕜) (a i)) f

The multivariate Gaussian Hermite expansion. Every f ∈ L²(γ^ι; 𝕜) is the sum of its multi-index Hermite series, summed over multi-indices a : ι → ℕ in the unordered sense.