English
For any k ∈ ℕ, p ∈ R[X], and m ∈ ℕ, the coefficient of m in the k-th derivative of p equals (m+k).descFactorial(k) times the coefficient of m+k in p:
Русский
Для любых k ∈ ℕ, p ∈ R[X] и m ∈ ℕ, коэффициент при m в k-й производной p равен (m+k).descFactorial(k) умножить на коэффициент p при (m+k).
LaTeX
$$$$ (\operatorname{coeff}((\operatorname{derivative})^{k} p))(m) = (m + k).\operatorname{descFactorial} k \cdot (\operatorname{coeff}(p))(m + k) $$$$
Lean4
theorem coeff_iterate_derivative {k} (p : R[X]) (m : ℕ) :
(derivative^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k) := by
induction k generalizing m with
| zero => simp
| succ k ih =>
calc
(derivative^[k + 1] p).coeff m
_ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
_ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
_ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
_ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by rw [Nat.succ_add_eq_add_succ]
