Parseval and coordinates for the Hermite basis of L²(ℝ)

TauCeti.hermiteHilbertBasis exhibits the Hermite functions as a Hilbert basis of L²(ℝ; 𝕜). This file states the expansion identities that basis was built for, phrased in terms of the explicit vectors TauCeti.hermiteFunctionLp rather than the bundled basis, so that a consumer never has to unfold hermiteHilbertBasis to expand a function in Hermite functions.

Main statements

• TauCeti.hermiteHilbertBasis_repr_apply — the n-th coordinate of f is ⟪ψₙ, f⟫.
• TauCeti.tsum_inner_mul_inner_hermiteFunctionLp — Parseval in polarized form, ∑' n, ⟪f, ψₙ⟫ * ⟪ψₙ, g⟫ = ⟪f, g⟫.
• TauCeti.tsum_norm_sq_inner_hermiteFunctionLp — Parseval in norm-square form, ∑' n, ‖⟪ψₙ, f⟫‖² = ‖f‖².
• TauCeti.hermiteHilbertBasis_repr_self — the coordinates of a basis vector are a single 1.
• TauCeti.hasSum_hermiteFunctionLp_expansion — the Hermite expansion ∑' n, ⟪ψₙ, f⟫ • ψₙ = f.

Every statement holds for an arbitrary RCLike scalar field, so 𝕜 = ℝ and 𝕜 = ℂ are the same theorem. The roadmap OrthogonalL2Bases Part A3 acceptance criteria on the coordinates and norm of ψ₀ follow by instantiating hermiteHilbertBasis_repr_self and tsum_norm_sq_inner_hermiteFunctionLp at f = ψ₀, together with norm_hermiteFunctionLp_zero; no separate declaration is needed for that specialization.

@[simp]

theorem TauCeti.hermiteHilbertBasis_repr_apply {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) (n : ℕ) : ↑((hermiteHilbertBasis 𝕜).repr f) n = inner 𝕜 (hermiteFunctionLp 𝕜 n) f

The coordinates of f in the Hermite basis are its inner products against the Hermite functions.

theorem TauCeti.tsum_inner_mul_inner_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] (f g : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) : ∑' (n : ℕ), inner 𝕜 f (hermiteFunctionLp 𝕜 n) * inner 𝕜 (hermiteFunctionLp 𝕜 n) g = inner 𝕜 f g

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

theorem TauCeti.tsum_norm_sq_inner_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) : ∑' (n : ℕ), ‖inner 𝕜 (hermiteFunctionLp 𝕜 n) f‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the Hermite basis (norm-square form): the squared Hermite coordinates of f sum to ‖f‖². This is the roadmap's Part A3 acceptance criterion.

theorem TauCeti.summable_norm_sq_inner_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) : Summable fun (n : ℕ) => ‖inner 𝕜 (hermiteFunctionLp 𝕜 n) f‖ ^ 2

The squared Hermite coordinate family of an L² function is summable.

theorem TauCeti.hasSum_hermiteFunctionLp_expansion {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) : HasSum (fun (n : ℕ) => inner 𝕜 (hermiteFunctionLp 𝕜 n) f • hermiteFunctionLp 𝕜 n) f

The Hermite expansion. Every f ∈ L²(ℝ) is the sum of its Hermite series.

@[simp]

theorem TauCeti.hermiteHilbertBasis_repr_self {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) : (hermiteHilbertBasis 𝕜).repr (hermiteFunctionLp 𝕜 n) = lp.single 2 n 1

The coordinates of the n-th Hermite function are a single 1 in position n.