Theorems · Theorem · special functions

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.

Defined in

Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Cited by

1 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound