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

• Polynomial.deriv_gaussian_eq_hermite_mul_gaussian: The Hermite polynomial is (up to sign) the polynomial factor occurring in the nth derivative of a gaussian.

References

• Hermite Polynomials

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

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 : ℝ) => (-(y ^ 2 / 2)).exp) x / (-(x ^ 2 / 2)).exp

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