English
Derivative iterates of the Gaussian exp(−y^2/2) are, up to a sign, the Hermite polynomials times the Gaussian.
Русский
Пусть берётся n-й итеративной производной по Gaussian e^{−y^2/2}; она равна (до знака) эрмитовым полиномам, умноженным на Gaussian.
LaTeX
$$$\forall n, x:\; \frac{d^n}{dx^n} e^{-(x^2)/2} = (-1)^n \cdot aeval(x, \operatorname{hermite}(n)) \cdot e^{-(x^2)/2}$$$
Lean4
/-- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a Gaussian. -/
theorem deriv_gaussian_eq_hermite_mul_gaussian (n : ℕ) (x : ℝ) :
deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1 : ℝ) ^ n * aeval x (hermite n) * Real.exp (-(x ^ 2 / 2)) :=
by
rw [mul_assoc]
induction n generalizing x with
| zero => rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
| succ n ih =>
replace ih : deriv^[n] _ = _ := _root_.funext ih
have deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [mul_comm, ← neg_mul]`
rw [deriv_exp (by simp)]
simp [mul_comm]
rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ), deriv_gaussian,
hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
· ring
· apply Polynomial.differentiable_aeval
· apply DifferentiableAt.exp;
simp -- Porting note: was just `simp`
