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 : Nat) (x : Real) : Eq (Nat.iterate deriv n (fun (y : Real) => Real.exp (Neg.neg (HDiv.hDiv (HPow.hPow y 2) 2))) x) (HMul.hMul (HMul.hMul (HPow.hPow (-1) n) (DFunLike.coe (aeval x) (hermite n))) (Real.exp (Neg.neg (HDiv.hDiv (HPow.hPow 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 : Nat) (x : Real) : Eq (DFunLike.coe (aeval x) (hermite n)) (HDiv.hDiv (HMul.hMul (HPow.hPow (-1) n) (Nat.iterate deriv n (fun (y : Real) => Real.exp (Neg.neg (HDiv.hDiv (HPow.hPow y 2) 2))) x)) (Real.exp (Neg.neg (HDiv.hDiv (HPow.hPow x 2) 2))))

theorem Polynomial.hermite_eq_deriv_gaussian' (n : Nat) (x : Real) : Eq (DFunLike.coe (aeval x) (hermite n)) (HMul.hMul (HMul.hMul (HPow.hPow (-1) n) (Nat.iterate deriv n (fun (y : Real) => Real.exp (Neg.neg (HDiv.hDiv (HPow.hPow y 2) 2))) x)) (Real.exp (HDiv.hDiv (HPow.hPow x 2) 2)))