Parseval and expansions for the multi-index Hermite-function basis

TauCeti.hermiteFunctionPiBasis exhibits the multi-index Hermite functions Ψ_a(x) = ∏ᵢ ψ_{aᵢ}(xᵢ) as a Hilbert basis of L²(ℝ^ι). This file states the expansion identities that basis was built for, phrased in the explicit tensors TauCeti.L2piMul fun i => TauCeti.hermiteFunctionLp 𝕜 (a i) rather than the bundled basis, so that a consumer never has to unfold hermiteFunctionPiBasis to expand a function of several variables in Hermite functions. It is the Fintype-indexed analogue of TauCeti.tsum_norm_sq_inner_hermiteFunctionLp and its neighbours.

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 show that the coordinates of a product are the products of the one-dimensional Hermite coordinates.

Main statements

• TauCeti.hermiteFunctionPiBasis_repr_apply — the a-th coordinate of f is ⟪Ψ_a, f⟫.
• TauCeti.hermiteFunctionPiBasis_repr_eq_integral — the same coordinate as an integral against ∏ᵢ ψ_{aᵢ}(xᵢ), whose integrand is integrable by TauCeti.integrable_prod_hermiteFunction_mul.
• TauCeti.hermiteFunctionPiBasis_repr_L2piMul — the coordinates of a product function are the products of the one-dimensional coordinates.
• TauCeti.tsum_inner_mul_inner_L2piMul_hermiteFunctionLp — Parseval in polarized form.
• TauCeti.tsum_norm_sq_inner_L2piMul_hermiteFunctionLp — Parseval in norm-square form, ∑' a, ‖⟪Ψ_a, f⟫‖² = ‖f‖².
• TauCeti.hasSum_L2piMul_hermiteFunctionLp_expansion — the multi-index Hermite expansion ∑' a, ⟪Ψ_a, f⟫ • Ψ_a = f.

Every statement holds for an arbitrary RCLike scalar field, so 𝕜 = ℝ and 𝕜 = ℂ are the same theorem.

@[simp]

theorem TauCeti.hermiteFunctionPiBasis_repr_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume))) (a : ι → ℕ) : ↑((hermiteFunctionPiBasis 𝕜 ι).repr f) a = inner 𝕜 (L2piMul fun (i : ι) => hermiteFunctionLp 𝕜 (a i)) f

The coordinates of f in the multi-index Hermite-function basis are its inner products against the tensors Ψ_a = ∏ᵢ ψ_{aᵢ}.

theorem TauCeti.integrable_prod_hermiteFunction_mul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume))) (a : ι → ℕ) : MeasureTheory.Integrable (fun (x : ι → ℝ) => (∏ i : ι, (algebraMap ℝ 𝕜) (hermiteFunction (a i) (x i))) * ↑↑f x) (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume)

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

theorem TauCeti.hermiteFunctionPiBasis_repr_eq_integral {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume))) (a : ι → ℕ) : ↑((hermiteFunctionPiBasis 𝕜 ι).repr f) a = ∫ (x : ι → ℝ), (∏ i : ι, (algebraMap ℝ 𝕜) (hermiteFunction (a i) (x i))) * ↑↑f x ∂MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume

The a-th multi-index Hermite coordinate of f, as an integral of f against the product ∏ᵢ ψ_{aᵢ}(xᵢ). The Hermite functions are real, so no complex conjugate survives.

theorem TauCeti.hermiteFunctionPiBasis_repr_L2piMul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (F : ι → ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) (a : ι → ℕ) : ↑((hermiteFunctionPiBasis 𝕜 ι).repr (L2piMul F)) a = ∏ i : ι, inner 𝕜 (hermiteFunctionLp 𝕜 (a i)) (F i)

The multi-index coordinates of a product function factor. If f(x) = ∏ᵢ Fᵢ(xᵢ) then its a-th multi-index Hermite coordinate is the product of the aᵢ-th one-dimensional Hermite coordinates of the factors — the statement that makes a multidimensional Hermite expansion of a product function computable from one-dimensional ones.

Unlike its generic source TauCeti.piHilbertBasis_repr_L2piMul and its Gaussian sibling TauCeti.gaussianHermitePiBasis_repr_L2piMul, this is not a simp lemma: simp already factors this coordinate, through TauCeti.hermiteFunctionPiBasis_repr_apply and TauCeti.inner_L2piMul.

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

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

theorem TauCeti.tsum_norm_sq_inner_L2piMul_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume))) : ∑' (a : ι → ℕ), ‖inner 𝕜 (L2piMul fun (i : ι) => hermiteFunctionLp 𝕜 (a i)) f‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the multi-index Hermite basis (norm-square form): the squared multi-index Hermite coordinates of f sum to ‖f‖².

theorem TauCeti.summable_norm_sq_inner_L2piMul_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume))) : Summable fun (a : ι → ℕ) => ‖inner 𝕜 (L2piMul fun (i : ι) => hermiteFunctionLp 𝕜 (a i)) f‖ ^ 2

The squared multi-index Hermite coordinate family of an L²(ℝ^ι) function is summable.

theorem TauCeti.hasSum_L2piMul_hermiteFunctionLp_expansion {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume))) : HasSum (fun (a : ι → ℕ) => inner 𝕜 (L2piMul fun (i : ι) => hermiteFunctionLp 𝕜 (a i)) f • L2piMul fun (i : ι) => hermiteFunctionLp 𝕜 (a i)) f

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