hermite_eq_iterate — Mathlib

English

The Hermite polynomial of degree n is obtained by applying the operator T(p) = X p − p' n times to the constant 1.

Русский

Полином Эрмита степени n получается путём применения оператора T(p) = X p − p' n раз к константе 1.

LaTeX

$$$\operatorname{hermite}(n) = T^{[n]}(1),\quad T(p)=X\cdot p - p',$$$

Lean4

theorem hermite_eq_iterate (n : ℕ) : hermite n = (fun p => X * p - derivative p)^[n] 1 := by
  induction n with
  | zero => rfl
  | succ n ih => rw [Function.iterate_succ_apply', ← ih, hermite_succ]

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