hermite_succ — Mathlib

English

The Hermite polynomial satisfies the recurrence h_{n+1} = x h_n − h'_n.

Русский

Полином Эрмита удовлетворяет рекуррентному соотношению h_{n+1} = x h_n − h'_n.

LaTeX

$$$\operatorname{hermite}(n+1) = X \cdot \operatorname{hermite}(n) - \operatorname{derivative}(\operatorname{hermite}(n)).$$$

Lean4

/-- The recursion `hermite (n+1) = (x - d/dx) (hermite n)` -/
@[simp]
theorem hermite_succ (n : ℕ) : hermite (n + 1) = X * hermite n - derivative (hermite n) := by rw [hermite]

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