The harmonic-oscillator eigen-equation for the Hermite functions

This file adds the A2 oscillator milestone of the OrthogonalL2Bases roadmap: the Hermite functions ψₙ (TauCeti.hermiteFunction, ψₙ(x) = Hₙ(x√2) exp(-x²/2) / √(n!√π)) are the eigenfunctions of the quantum harmonic oscillator,

-ψₙ'' + x²·ψₙ = (2n+1)·ψₙ.

The whole argument stays at the pointwise level and is built directly on the creation and annihilation identities proved in TauCeti.Analysis.SpecialFunctions.Hermite.Function.Ladder:

• TauCeti.mul_sub_deriv_hermiteFunction — x·ψₙ - ψₙ' = √(2(n+1))·ψ_{n+1} (creation);
• TauCeti.mul_add_deriv_hermiteFunction — x·ψₙ + ψₙ' = √(2n)·ψ_{n-1} (annihilation).

Writing c = √(2(n+1)), the creation identity gives ψₙ' = x·ψₙ - c·ψ_{n+1}, so differentiating once more (product rule) and eliminating ψ_{n+1}' through the annihilation identity at index n+1 (x·ψ_{n+1} + ψ_{n+1}' = c·ψₙ, since √(2(n+1)) is again c) collapses every neighbouring mode, using only c² = 2(n+1):

ψₙ'' = ψₙ + x·ψₙ' - c·ψ_{n+1}' = x²·ψₙ - (2n+1)·ψₙ.

The main results are the closed form of the second derivative, TauCeti.deriv_deriv_hermiteFunction (ψₙ'' = (x² - (2n+1))·ψₙ), and the eigen-equation TauCeti.hermiteFunction_oscillator in the roadmap's -ψₙ'' + x²·ψₙ = (2n+1)·ψₙ form.

No case split on n is needed: the neighbour that would require the Nat-clamped index n-1 never enters, because the derivation uses the creation identity at n and the annihilation identity at n+1, whose lower index (n+1)-1 = n is exact.

theorem TauCeti.hasDerivAt_deriv_hermiteFunction (n : ℕ) (x : ℝ) : HasDerivAt (deriv (hermiteFunction n)) ((x ^ 2 - (2 * ↑n + 1)) * hermiteFunction n x) x

Second derivative of the Hermite function (the derivative form). The Hermite function ψₙ solves ψₙ'' = (x² - (2n+1))·ψₙ; this states that the derivative of ψₙ' at x equals (x² - (2n+1))·ψₙ(x).

@[simp]

theorem TauCeti.deriv_deriv_hermiteFunction (n : ℕ) (x : ℝ) : deriv (deriv (hermiteFunction n)) x = (x ^ 2 - (2 * ↑n + 1)) * hermiteFunction n x

Second derivative of the Hermite function. ψₙ'' = (x² - (2n+1))·ψₙ; the closed form behind the harmonic-oscillator eigen-equation.

theorem TauCeti.hermiteFunction_oscillator (n : ℕ) (x : ℝ) : -deriv (deriv (hermiteFunction n)) x + x ^ 2 * hermiteFunction n x = (2 * ↑n + 1) * hermiteFunction n x

The harmonic-oscillator eigen-equation. The Hermite function ψₙ is an eigenfunction of the Schrödinger operator -d²/dx² + x² with eigenvalue 2n+1:

-ψₙ'' + x²·ψₙ = (2n+1)·ψₙ.

@[simp]

theorem TauCeti.iteratedDeriv_two_hermiteFunction (n : ℕ) (x : ℝ) : iteratedDeriv 2 (hermiteFunction n) x = (x ^ 2 - (2 * ↑n + 1)) * hermiteFunction n x

The oscillator eigen-equation phrased with iteratedDeriv 2.