Ladder and harmonic-oscillator operators on Schwartz space

This file packages the Hermite creation and annihilation operators as continuous linear operators on the real Schwartz space 𝓢(ℝ, ℝ), proves their canonical commutation relation (CCR) [a, a†] = id, and establishes their spectral properties on the family of Hermite Schwartz functions TauCeti.hermiteSchwartzMap n.

Main declarations

• TauCeti.hermiteAnnihilationCLM — the annihilation operator a = (x + d/dx) / √2.
• TauCeti.hermiteCreationCLM — the creation operator a† = (x - d/dx) / √2.
• The canonical commutation relation [a, a†] = id (a ∘L a† - a† ∘L a = id).
• TauCeti.hermiteAnnihilationCLM_apply_hermiteSchwartzMap — a ψₙ = √n • ψ_{n-1}.
• TauCeti.hermiteCreationCLM_apply_hermiteSchwartzMap — a† ψₙ = √(n+1) • ψ_{n+1}.
• TauCeti.hermiteNumberCLM — the number operator N = a† ∘L a.
• TauCeti.hermiteNumberCLM_apply_hermiteSchwartzMap — N ψₙ = n • ψₙ.
• TauCeti.hermiteOscillatorCLM — the harmonic oscillator operator H = N + (1/2) • id.
• TauCeti.hermiteOscillatorCLM_apply_apply — the differential action of H.
• TauCeti.hermiteOscillatorCLM_apply_hermiteSchwartzMap — H ψₙ = (n + 1/2) • ψₙ.

Reference

Roadmap: OrthogonalL2Bases, Part A2 (ladder operators on Schwartz space / L²).

noncomputable def TauCeti.hermiteAnnihilationCLM : SchwartzMap ℝ ℝ →L[ℝ] SchwartzMap ℝ ℝ

The annihilation operator a = (x + d/dx) / √2 as a continuous linear operator on the real Schwartz space 𝓢(ℝ, ℝ).

Equations

• TauCeti.hermiteAnnihilationCLM = (√2)⁻¹ • ((SchwartzMap.smulLeftCLM ℝ fun (x : ℝ) => x) + SchwartzMap.derivCLM ℝ ℝ)

noncomputable def TauCeti.hermiteCreationCLM : SchwartzMap ℝ ℝ →L[ℝ] SchwartzMap ℝ ℝ

The creation operator a† = (x - d/dx) / √2 as a continuous linear operator on the real Schwartz space 𝓢(ℝ, ℝ).

Equations

• TauCeti.hermiteCreationCLM = (√2)⁻¹ • ((SchwartzMap.smulLeftCLM ℝ fun (x : ℝ) => x) - SchwartzMap.derivCLM ℝ ℝ)

@[simp]

theorem TauCeti.hermiteAnnihilationCLM_apply_apply (f : SchwartzMap ℝ ℝ) (x : ℝ) : (hermiteAnnihilationCLM f) x = (√2)⁻¹ * (x * f x + deriv (⇑f) x)

Pointwise evaluation of the annihilation operator a f.

@[simp]

theorem TauCeti.hermiteCreationCLM_apply_apply (f : SchwartzMap ℝ ℝ) (x : ℝ) : (hermiteCreationCLM f) x = (√2)⁻¹ * (x * f x - deriv (⇑f) x)

Pointwise evaluation of the creation operator a† f.

@[simp]

theorem TauCeti.hermiteAnnihilationCLM_apply_hermiteSchwartzMap (n : ℕ) : hermiteAnnihilationCLM (hermiteSchwartzMap n) = √↑n • hermiteSchwartzMap (n - 1)

Annihilation action on Hermite functions. a (hermiteSchwartzMap n) = √n • hermiteSchwartzMap (n - 1).

@[simp]

theorem TauCeti.hermiteCreationCLM_apply_hermiteSchwartzMap (n : ℕ) : hermiteCreationCLM (hermiteSchwartzMap n) = √(↑n + 1) • hermiteSchwartzMap (n + 1)

Creation action on Hermite functions. a† (hermiteSchwartzMap n) = √(n + 1) • hermiteSchwartzMap (n + 1).

@[simp]

theorem TauCeti.hermiteAnnihilationCLM_comp_hermiteCreationCLM_sub_hermiteCreationCLM_comp_hermiteAnnihilationCLM : hermiteAnnihilationCLM ∘SL hermiteCreationCLM - hermiteCreationCLM ∘SL hermiteAnnihilationCLM = ContinuousLinearMap.id ℝ (SchwartzMap ℝ ℝ)

Canonical Commutation Relation (CCR) for the Hermite ladder operators. [a, a†] = a ∘L a† - a† ∘L a = id.

noncomputable def TauCeti.hermiteNumberCLM : SchwartzMap ℝ ℝ →L[ℝ] SchwartzMap ℝ ℝ

The Hermite number operator N = a† ∘L a as a continuous linear operator on 𝓢(ℝ, ℝ).

Equations

• TauCeti.hermiteNumberCLM = TauCeti.hermiteCreationCLM ∘SL TauCeti.hermiteAnnihilationCLM

@[simp]

theorem TauCeti.hermiteNumberCLM_apply_apply (f : SchwartzMap ℝ ℝ) (x : ℝ) : (hermiteNumberCLM f) x = ((x ^ 2 - 1) * f x - deriv (deriv ⇑f) x) / 2

Pointwise differential action of the number operator: Nf = (x²f - f - f'') / 2.

@[simp]

theorem TauCeti.hermiteNumberCLM_apply_hermiteSchwartzMap (n : ℕ) : hermiteNumberCLM (hermiteSchwartzMap n) = ↑n • hermiteSchwartzMap n

Action of the number operator on Hermite functions. N (hermiteSchwartzMap n) = n • hermiteSchwartzMap n.

noncomputable def TauCeti.hermiteOscillatorCLM : SchwartzMap ℝ ℝ →L[ℝ] SchwartzMap ℝ ℝ

The harmonic oscillator operator H = N + (1/2) • id as a continuous linear operator on 𝓢(ℝ, ℝ).

Equations

• TauCeti.hermiteOscillatorCLM = TauCeti.hermiteNumberCLM + (1 / 2) • ContinuousLinearMap.id ℝ (SchwartzMap ℝ ℝ)

@[simp]

theorem TauCeti.hermiteOscillatorCLM_apply_apply (f : SchwartzMap ℝ ℝ) (x : ℝ) : (hermiteOscillatorCLM f) x = (-deriv (deriv ⇑f) x + x ^ 2 * f x) / 2

Pointwise differential action of the harmonic oscillator operator: Hf = (-f'' + x²f) / 2.

@[simp]

theorem TauCeti.hermiteOscillatorCLM_apply_hermiteSchwartzMap (n : ℕ) : hermiteOscillatorCLM (hermiteSchwartzMap n) = (↑n + 1 / 2) • hermiteSchwartzMap n

Action of the harmonic oscillator operator on Hermite functions. H (hermiteSchwartzMap n) = (n + 1/2) • hermiteSchwartzMap n.