Documentation

TauCeti.Analysis.SpecialFunctions.Hermite.Function.Basic

Basic Hermite functions #

This file starts the object API for the Hermite functions used by the OrthogonalL2Bases roadmap. The nth function is the normalized probabilists' Hermite polynomial evaluated at x * sqrt 2, multiplied by the Gaussian envelope exp (-x^2 / 2).

The API here is deliberately pointwise: the definition, continuity and smoothness, the first three base formulas ψ₀, ψ₁, and ψ₂, and the parity formula ψₙ(-x) = (-1)ⁿ ψₙ(x). Orthogonality, L² packaging, and the oscillator identities are later milestones built on this basic object.

source
noncomputable def TauCeti.hermiteFunction (n : ℕ) (x : ℝ) :
ℝ

The real Hermite function ψₙ(x) = Hₙ(x√2) exp(-x² / 2) / sqrt(n! sqrt π), using Mathlib's probabilists' Hermite polynomial Polynomial.hermite.

Equations
Instances For
    source
    theorem TauCeti.hermiteFunction_def (n : ℕ) (x : ℝ) :
    hermiteFunction n x = (Polynomial.aeval (x * √2)) (Polynomial.hermite n) * Real.exp (-(x ^ 2 / 2)) / √(↑n.factorial * √Real.pi)

    The defining equation for the real Hermite function.

    source
    theorem TauCeti.sqrt_factorial_mul_sqrt_pi_pos (n : ℕ) :
    0 < √(↑n.factorial * √Real.pi)

    The square root normalization factor in the Hermite function is positive.

    source
    theorem TauCeti.sqrt_factorial_mul_sqrt_pi_ne_zero (n : ℕ) :
    √(↑n.factorial * √Real.pi) ≠ 0

    The square root normalization factor in the Hermite function is nonzero.

    source
    theorem TauCeti.continuous_hermiteFunction (n : ℕ) :
    Continuous (hermiteFunction n)

    The real Hermite functions are continuous.

    source
    theorem TauCeti.contDiff_hermiteFunction (n : ℕ) :
    ContDiff ℝ ⊤ (hermiteFunction n)

    The real Hermite functions are smooth.

    source
    @[simp]
    theorem TauCeti.hermiteFunction_zero (x : ℝ) :
    hermiteFunction 0 x = Real.exp (-(x ^ 2 / 2)) / √√Real.pi

    The zeroth Hermite function is the Gaussian divided by sqrt (sqrt π).

    source
    @[simp]
    theorem TauCeti.hermiteFunction_one (x : ℝ) :
    hermiteFunction 1 x = √2 * x * hermiteFunction 0 x

    The first Hermite function is sqrt 2 * x times the zeroth Hermite function.

    source
    theorem TauCeti.hermiteFunction_one_eq (x : ℝ) :
    hermiteFunction 1 x = √2 * x * Real.exp (-(x ^ 2 / 2)) / √√Real.pi

    The first Hermite function as an explicit scalar multiple of the Gaussian envelope.

    source
    theorem TauCeti.hermiteFunction_two (x : ℝ) :
    hermiteFunction 2 x = ((x * √2) ^ 2 - 1) * Real.exp (-(x ^ 2 / 2)) / √(2 * √Real.pi)

    The second Hermite function in pointwise form.

    Parity #

    source
    @[simp]
    theorem TauCeti.hermiteFunction_neg (n : ℕ) (x : ℝ) :
    hermiteFunction n (-x) = (-1) ^ n * hermiteFunction n x

    Target A2 (parity). ψₙ(-x) = (-1)ⁿ ψₙ(x): the Gaussian envelope exp(-x²/2) is even and the polynomial factor Hₙ(x√2) carries the parity of Hₙ (Polynomial.hermite_aeval_neg).