Hermite functions in Schwartz space

This file packages the real Hermite functions as Schwartz functions. The construction first shows directly that the Gaussian x ↦ exp (-x² / 2) is rapidly decreasing, using Mathlib's formula for all of its derivatives in terms of Hermite polynomials. Multiplication by the polynomial factor then uses SchwartzMap.smulLeftCLM.

The resulting hermiteSchwartzMap has hermiteFunction as its underlying function. The pointwise position and derivative ladder relations are also recorded as equalities in Schwartz space, so later constructions can use Mathlib's continuous operators on 𝓢(ℝ, ℝ).

noncomputable def TauCeti.hermiteSchwartzMap (n : ℕ) : SchwartzMap ℝ ℝ

The nth Hermite function, as an element of the real Schwartz space 𝓢(ℝ, ℝ).

Equations

• TauCeti.hermiteSchwartzMap n = (SchwartzMap.smulLeftCLM ℝ fun (x : ℝ) => (Polynomial.aeval (x * √2)) (Polynomial.hermite n) / √(↑n.factorial * √Real.pi)) TauCeti.gaussianSchwartzMap✝

@[simp]

theorem TauCeti.hermiteSchwartzMap_apply (n : ℕ) (x : ℝ) : (hermiteSchwartzMap n) x = hermiteFunction n x

The underlying function of hermiteSchwartzMap n is hermiteFunction n.

@[simp]

theorem TauCeti.coe_hermiteSchwartzMap (n : ℕ) : ⇑(hermiteSchwartzMap n) = hermiteFunction n

The coercion of hermiteSchwartzMap n is the pointwise Hermite function.

@[simp]

theorem TauCeti.mul_hermiteSchwartzMap (n : ℕ) : (SchwartzMap.smulLeftCLM ℝ fun (x : ℝ) => x) (hermiteSchwartzMap n) = √((↑n + 1) / 2) • hermiteSchwartzMap (n + 1) + √(↑n / 2) • hermiteSchwartzMap (n - 1)

The position ladder relation, as an equality in Schwartz space.

@[simp]

theorem TauCeti.deriv_hermiteSchwartzMap (n : ℕ) : (SchwartzMap.derivCLM ℝ ℝ) (hermiteSchwartzMap n) = √(↑n / 2) • hermiteSchwartzMap (n - 1) - √((↑n + 1) / 2) • hermiteSchwartzMap (n + 1)

The derivative ladder relation, as an equality in Schwartz space.

theorem TauCeti.mul_add_deriv_hermiteSchwartzMap (n : ℕ) : (SchwartzMap.smulLeftCLM ℝ fun (x : ℝ) => x) (hermiteSchwartzMap n) + (SchwartzMap.derivCLM ℝ ℝ) (hermiteSchwartzMap n) = √(2 * ↑n) • hermiteSchwartzMap (n - 1)

The annihilation relation, as an equality in Schwartz space.

theorem TauCeti.mul_sub_deriv_hermiteSchwartzMap (n : ℕ) : (SchwartzMap.smulLeftCLM ℝ fun (x : ℝ) => x) (hermiteSchwartzMap n) - (SchwartzMap.derivCLM ℝ ℝ) (hermiteSchwartzMap n) = √(2 * (↑n + 1)) • hermiteSchwartzMap (n + 1)

The creation relation, as an equality in Schwartz space.