coeff_hermite_succ_succ — Mathlib

English

For all n, k, the coefficient satisfies a two-step recurrence: coeff(hermite(n+1))(k+1) = coeff(hermite(n)) (k) − (k+2)·coeff(hermite(n))(k+2).

Русский

Для всех n, k коэффициент удовлетворяет двумерному рекуррентному relation: coeff(hermite(n+1))(k+1) = coeff(hermite(n))(k) − (k+2)·coeff(hermite(n))(k+2).

LaTeX

$$$\forall n,k\,\;\operatorname{coeff}(\operatorname{hermite}(n+1),k+1) = \operatorname{coeff}(\operatorname{hermite}(n),k) - (k+2) \cdot \operatorname{coeff}(\operatorname{hermite}(n),k+2).$$$

Lean4

theorem coeff_hermite_succ_succ (n k : ℕ) :
    coeff (hermite (n + 1)) (k + 1) = coeff (hermite n) k - (k + 2) * coeff (hermite n) (k + 2) :=
  by
  rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]
  norm_cast

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