hermite_eq_deriv_gaussian' — Mathlib

English

An identity connecting Hermite polynomials with Gaussian function via derivatives and exponentials: h(n)(x) relates to exp(−(x^2)/2) times a derivative of exp(x^2/2).

Русский

Связь полиномов Эрмита с гауссовской функцией через производные и экспоненты: h_n(x) связаны с производной и экспонентой exp(x^2/2).

LaTeX

$$$\\mathrm{aeval}\n x\\ (\\text{явление})\\; (\\text{гладкость})$$$

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 [hermite_eq_deriv_gaussian, Real.exp_neg]
  field_simp

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