The multi-index Hermite-function basis of L²(ℝ^ι)

The Fintype-indexed product of the one-dimensional Hermite-function basis: the multi-index family Ψ_a(x) = ∏ᵢ ψ_{aᵢ}(xᵢ) is a Hilbert basis of L²(volume^ι), the standard eigenbasis of the ℝ^ι harmonic oscillator.

This is the Lebesgue-product-measure sibling of TauCeti.gaussianHermitePiBasis (which carries the Gaussian in the measure). Both are TauCeti.piHilbertBasis over their respective one-dimensional factor — here TauCeti.hermiteHilbertBasis — so this file only performs the assembly.

Main statements

• TauCeti.hermiteFunctionPiBasis — the multi-index basis.
• TauCeti.hermiteFunctionPiBasis_apply — the a-th vector is the tensor TauCeti.L2piMul of the one-dimensional Hermite vectors, as an equality of L² vectors.
• TauCeti.coeFn_hermiteFunctionPiBasis — the anti-vacuity pin: the a-th vector really is the product ∏ᵢ ψ_{aᵢ}(xᵢ).

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

The multidimensional Hermite-function basis. piHilbertBasis over the one-dimensional Hermite-function basis in every coordinate — the eigenbasis of the ℝ^ι harmonic oscillator.

Equations

• TauCeti.hermiteFunctionPiBasis 𝕜 ι = TauCeti.piHilbertBasis fun (x : ι) => TauCeti.hermiteHilbertBasis 𝕜

@[simp]

theorem TauCeti.hermiteFunctionPiBasis_apply (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] (a : ι → ℕ) : (hermiteFunctionPiBasis 𝕜 ι) a = L2piMul fun (i : ι) => hermiteFunctionLp 𝕜 (a i)

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

theorem TauCeti.coeFn_hermiteFunctionPiBasis (𝕜 : Type u_1) [RCLike 𝕜] (ι : Type u_2) [Fintype ι] (a : ι → ℕ) : ↑↑((hermiteFunctionPiBasis 𝕜 ι) a) =ᵐ[MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume] fun (x : ι → ℝ) => ∏ i : ι, (algebraMap ℝ 𝕜) (hermiteFunction (a i) (x i))

The basis vectors are the multi-index Hermite-function products. Without this the construction would only exhibit some Hilbert basis of L²(volume^ι). The coordinatewise identification ⇑(hermiteHilbertBasis 𝕜) = hermiteFunctionLp 𝕜 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).