Hermite functions as L² vectors

This file packages the pointwise Hermite functions TauCeti.hermiteFunction n as elements of Lp 𝕜 2 volume, for any RCLike scalar field 𝕜. This is the hermiteFunctionLp family named in the OrthogonalL2Bases roadmap's Part A3: the later orthonormality and Hilbert-basis theorems use these Lp vectors, while the analytic L² membership is supplied by TauCeti.memLp_two_hermiteFunction.

The a.e. representative lemmas are the anti-vacuity pins for downstream consumers: they expose that the bundled Lp vectors are exactly the scalar casts of the explicit pointwise functions.

theorem TauCeti.inner_algebraMap_algebraMap {𝕜 : Type u_1} [RCLike 𝕜] (a b : ℝ) : inner 𝕜 ((algebraMap ℝ 𝕜) a) ((algebraMap ℝ 𝕜) b) = (algebraMap ℝ 𝕜) (a * b)

The inner product of two real scalar casts is the scalar cast of their product.

Scalar-cast L² membership

theorem TauCeti.memLp_two_algebraMap_hermiteFunction {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (hermiteFunction n x)) 2 MeasureTheory.volume

The 𝕜-valued scalar cast of a Hermite function lies in L²(volume).

Lp packaging

noncomputable def TauCeti.hermiteFunctionLp (𝕜 : Type u_2) [RCLike 𝕜] (n : ℕ) : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)

The nth Hermite function as a vector of L²(ℝ, volume; 𝕜), with the real pointwise function cast through algebraMap ℝ 𝕜.

Equations

• TauCeti.hermiteFunctionLp 𝕜 n = MeasureTheory.MemLp.toLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (TauCeti.hermiteFunction n x)) ⋯

theorem TauCeti.coeFn_hermiteFunctionLp {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) : ↑↑(hermiteFunctionLp 𝕜 n) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => (algebraMap ℝ 𝕜) (hermiteFunction n x)

The Lp representative of hermiteFunctionLp is the scalar cast of the pointwise Hermite function.

theorem TauCeti.coeFn_hermiteFunctionLp_real (n : ℕ) : ↑↑(hermiteFunctionLp ℝ n) =ᵐ[MeasureTheory.volume] hermiteFunction n

In real scalars, hermiteFunctionLp has the original pointwise Hermite function as an a.e. representative.

Zeroth-mode normalization

theorem TauCeti.inner_hermiteFunctionLp_zero_zero {𝕜 : Type u_1} [RCLike 𝕜] : inner 𝕜 (hermiteFunctionLp 𝕜 0) (hermiteFunctionLp 𝕜 0) = 1

The zeroth Lp Hermite function has inner product one with itself, over any RCLike scalar field. This lower-level result is available without importing the full orthonormality development.

@[simp]

theorem TauCeti.norm_hermiteFunctionLp_zero {𝕜 : Type u_1} [RCLike 𝕜] : ‖hermiteFunctionLp 𝕜 0‖ = 1

The zeroth Lp Hermite function is a unit vector, over any RCLike scalar field. This lower-level result is available without importing the full orthonormality development. It has high simp priority so it remains the preferred zeroth-mode rule when the general theorem is also imported.