hermite_eq_deriv_gaussian — Mathlib

English

There is a precise identity linking aeval x (hermite n) with the nth derivative iterates of the Gaussian, via a quotient by e^{−x^2/2}.

Русский

Существует точное тождество, связывающее aeval x (hermite n) с через n-ю производную от гауссиана, делённое на e^{−x^2/2}.

LaTeX

$$$\forall n,x:\; aeval\,x\,(\operatorname{hermite}(n)) = (-1)^n \cdot \dfrac{\operatorname{deriv}^{\,n}\big( e^{-(y^2/2)} \big)\,|_{y=x}}{e^{-(x^2/2)}}$$$

Lean4

theorem hermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
    aeval x (hermite n) = (-1 : ℝ) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2)) :=
  by
  rw [deriv_gaussian_eq_hermite_mul_gaussian]
  field_simp
  rw [← pow_mul]
  simp

Похожие утверждения