Documentation

Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Hermite polynomials and Gaussians #

This file shows that the Hermite polynomial hermite n is (up to sign) the polynomial factor occurring in the nth derivative of a gaussian.

Results #

References #

theorem Polynomial.deriv_gaussian_eq_hermite_mul_gaussian (n : ) (x : ) :
deriv^[n] (fun (y : ) => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (Polynomial.aeval x) (Polynomial.hermite n) * Real.exp (-(x ^ 2 / 2))

hermite n is (up to sign) the factor appearing in deriv^[n] of a gaussian

theorem Polynomial.hermite_eq_deriv_gaussian (n : ) (x : ) :
(Polynomial.aeval x) (Polynomial.hermite n) = (-1) ^ n * deriv^[n] (fun (y : ) => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))
theorem Polynomial.hermite_eq_deriv_gaussian' (n : ) (x : ) :
(Polynomial.aeval x) (Polynomial.hermite n) = (-1) ^ n * deriv^[n] (fun (y : ) => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)