Polynomial.deriv_gaussian_eq_hermite_mul_gaussian

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

The theorem `Polynomial.deriv_gaussian_eq_hermite_mul_gaussian` states that for every natural number `n` and real number `x`, the `n`th derivative of the Gaussian function, i.e., `exp(-(y ^ 2 / 2))`, evaluated at `x` is equal to the product of `(-1) ^ n`, the evaluation of the `n`th probabilists' Hermite polynomial at `x`, and the Gaussian function evaluated at `x`. In mathematical terms, $\frac{d^n}{dx^n} e^{-\frac{x^2}{2}} = (-1)^n H_n(x)e^{-\frac{x^2}{2}}$, where $H_n(x)$ denotes the `n`th Hermite polynomial.

More concisely: The `n`th derivative of the Gaussian function `exp(-(x ^ 2 / 2))` is equal to `(-1) ^ n` times the `n`th Hermite polynomial `H_n(x)` evaluated at `x`, multiplied by the Gaussian function `exp(-(x ^ 2 / 2)`.