mathlib3 documentation

ring_theory.polynomial.hermite.gaussian

Hermite polynomials and Gaussians #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
theorem polynomial.deriv_gaussian_eq_hermite_mul_gaussian (n : ℕ) (x : ℝ) :
deriv^[n] (λ (y : ℝ), rexp (-(y ^ 2 / 2))) x = (-1) ^ n * ⇑(polynomial.aeval x) (polynomial.hermite n) * rexp (-(x ^ 2 / 2))

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

source
theorem polynomial.hermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
⇑(polynomial.aeval x) (polynomial.hermite n) = (-1) ^ n * deriv^[n] (λ (y : ℝ), rexp (-(y ^ 2 / 2))) x / rexp (-(x ^ 2 / 2))
source
theorem polynomial.hermite_eq_deriv_gaussian' (n : ℕ) (x : ℝ) :
⇑(polynomial.aeval x) (polynomial.hermite n) = (-1) ^ n * deriv^[n] (λ (y : ℝ), rexp (-(y ^ 2 / 2))) x * rexp (x ^ 2 / 2)