derivative_iterate_coeff — Mathlib

English

The nth coefficient of the k-th derivative equals (descPochhammer ℤ k).smeval (n + k) times the (n + k)-th coefficient of f:

Русский

n-ый коэффициент k-й производной равен (descPochhammer ℤ k).smeval (n + k) умножить на (n + k)-й коэффициент f.

LaTeX

$$$\big((\mathrm{derivative}(R))^{[k]} f\big)_{n} = (\mathrm{descPochhammer}\; \mathbb{Z}\, k)^{\mathrm{smeval}}(n+k) \cdot f_{n+k}$$$

Lean4

@[simp]
theorem derivative_iterate_coeff (k : ℕ) (f : LaurentSeries V) (n : ℤ) :
    ((derivative R)^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + k) • f.coeff (n + k) := by
  rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff, Ring.descPochhammer_eq_factorial_smul_choose,
    smul_assoc]

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