Documentation

TauCeti.Analysis.SpecialFunctions.Hermite.Function.Fourier.Basic

Hermite functions as Fourier eigenfunctions #

Mathlib's Fourier transform uses the character exp (-2πixξ), whereas the Hermite functions TauCeti.hermiteFunction use the angular-frequency normalization. This file introduces the unitarily rescaled family

Φₙ(x) = √(√(2π)) ψₙ(√(2π)x)

and proves that 𝓕 Φₙ = (-i)ⁿ Φₙ. The dilation is load-bearing: the unscaled Gaussian exp (-x² / 2) is not self-dual for Mathlib's Fourier convention, while exp (-πx²) is.

Main statements #

The L² counterpart — the family as a Hilbert basis of L²(ℝ), diagonalizing the unitary Fourier transform — is in TauCeti.Analysis.SpecialFunctions.Hermite.Function.Fourier.HilbertBasis.

References #

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

The Hermite function rescaled to Mathlib's exp (-2πixξ) Fourier convention: Φₙ(x) = √(√(2π)) ψₙ(√(2π)x). The outer factor makes the dilation unitary on L².

Equations
Instances For
    source
    theorem TauCeti.twoPiHermiteFunction_def (n : ℕ) (x : ℝ) :
    twoPiHermiteFunction n x = √√(2 * Real.pi) * hermiteFunction n (√(2 * Real.pi) * x)

    The defining equation for the Hermite function rescaled to Mathlib's Fourier convention.

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

    The zeroth rescaled Hermite function is a constant multiple of the self-dual Gaussian exp (-πx²).

    source
    theorem TauCeti.continuous_twoPiHermiteFunction (n : ℕ) :
    Continuous (twoPiHermiteFunction n)

    The rescaled Hermite functions are continuous.

    source
    theorem TauCeti.mul_twoPiHermiteFunction (n : ℕ) (x : ℝ) :
    x * twoPiHermiteFunction n x = √((↑n + 1) / 2) / √(2 * Real.pi) * twoPiHermiteFunction (n + 1) x + √(↑n / 2) / √(2 * Real.pi) * twoPiHermiteFunction (n - 1) x

    The position ladder relation after the √(2π) dilation.

    source
    theorem TauCeti.hasDerivAt_twoPiHermiteFunction (n : ℕ) (x : ℝ) :
    HasDerivAt (twoPiHermiteFunction n) (√(2 * Real.pi) * (√(↑n / 2) * twoPiHermiteFunction (n - 1) x - √((↑n + 1) / 2) * twoPiHermiteFunction (n + 1) x)) x

    The derivative ladder relation after the √(2π) dilation.

    source
    @[simp]
    theorem TauCeti.deriv_twoPiHermiteFunction (n : ℕ) (x : ℝ) :
    deriv (twoPiHermiteFunction n) x = √(2 * Real.pi) * (√(↑n / 2) * twoPiHermiteFunction (n - 1) x - √((↑n + 1) / 2) * twoPiHermiteFunction (n + 1) x)

    The derivative form of hasDerivAt_twoPiHermiteFunction.

    source
    theorem TauCeti.mul_sub_invScale_deriv_twoPiHermiteFunction (n : ℕ) (x : ℝ) :
    √(2 * Real.pi) * x * twoPiHermiteFunction n x - (√(2 * Real.pi))⁻¹ * deriv (twoPiHermiteFunction n) x = √(2 * (↑n + 1)) * twoPiHermiteFunction (n + 1) x

    The creation relation for the rescaled family.

    source
    theorem TauCeti.integrable_twoPiHermiteFunction (n : ℕ) :
    MeasureTheory.Integrable (twoPiHermiteFunction n) MeasureTheory.volume

    Every rescaled Hermite function is integrable.

    source
    theorem TauCeti.fourier_twoPiHermiteFunction (n : ℕ) :
    (FourierTransform.fourier fun (x : ℝ) => ↑(twoPiHermiteFunction n x)) = fun (x : ℝ) => (-Complex.I) ^ n * ↑(twoPiHermiteFunction n x)

    Fourier eigenfunction theorem. For Mathlib's exp (-2πixξ) convention, the rescaled Hermite function Φₙ(x) = √(√(2π)) ψₙ(√(2π)x) has eigenvalue (-i)ⁿ.