Ladder relations for the Hermite functions

This file adds the A2 ladder relations of the OrthogonalL2Bases roadmap to the Hermite function object API (TauCeti.hermiteFunction, ψₙ(x) = Hₙ(x√2) exp(-x²/2) / √(n!√π)).

The two relations expose how the position operator x· and the derivative d/dx shift the Hermite index:

• TauCeti.mul_hermiteFunction — x·ψₙ = √((n+1)/2)·ψ_{n+1} + √(n/2)·ψ_{n-1};
• TauCeti.hasDerivAt_hermiteFunction (and its deriv form TauCeti.deriv_hermiteFunction) — ψₙ' = √(n/2)·ψ_{n-1} - √((n+1)/2)·ψ_{n+1}.

Adding and subtracting them yields the annihilation/creation identities for the ladder operators a = (x + d/dx)/√2 and a† = (x - d/dx)/√2:

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

All four relations are stated purely pointwise, with no integration involved. This is the level at which the roadmap wants these identities stated, so that they elevate to the ladder operators on 𝒮(ℝ) / L²(ℝ) later without re-proof.

The n = 0 boundary is covered by the √(n/2) = 0 coefficient, which annihilates the (Nat-clamped) ψ_{n-1} term, so the relations hold uniformly for all n : ℕ.

theorem TauCeti.mul_hermiteFunction (n : ℕ) (x : ℝ) : x * hermiteFunction n x = √((↑n + 1) / 2) * hermiteFunction (n + 1) x + √(↑n / 2) * hermiteFunction (n - 1) x

Target A2 (position ladder relation). Multiplying ψₙ by x mixes the neighbouring modes: x·ψₙ = √((n+1)/2)·ψ_{n+1} + √(n/2)·ψ_{n-1}.

theorem TauCeti.hasDerivAt_hermiteFunction (n : ℕ) (x : ℝ) : HasDerivAt (hermiteFunction n) (√(↑n / 2) * hermiteFunction (n - 1) x - √((↑n + 1) / 2) * hermiteFunction (n + 1) x) x

Target A2 (derivative ladder relation). Differentiating ψₙ mixes the neighbouring modes: ψₙ' = √(n/2)·ψ_{n-1} - √((n+1)/2)·ψ_{n+1}.

@[simp]

theorem TauCeti.deriv_hermiteFunction (n : ℕ) (x : ℝ) : deriv (hermiteFunction n) x = √(↑n / 2) * hermiteFunction (n - 1) x - √((↑n + 1) / 2) * hermiteFunction (n + 1) x

The deriv form of hasDerivAt_hermiteFunction.

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

Annihilation identity. The combination x·ψₙ + ψₙ' = √(2n)·ψ_{n-1}; this is the ladder operator a = (x + d/dx)/√2 acting as a ψₙ = √n·ψ_{n-1}.

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

Creation identity. The combination x·ψₙ - ψₙ' = √(2(n+1))·ψ_{n+1}; this is the ladder operator a† = (x - d/dx)/√2 acting as a† ψₙ = √(n+1)·ψ_{n+1}.