English
For p ∈ R[X] and k ∈ ℕ, the k-th derivative of p is given by a sum over its support: derivative^[k] p = sum over x in (derivative^[k] p).support of C((x+k).descFactorial k • p.coeff(x+k)) · X^x.
Русский
Для p ∈ R[X] и k ∈ ℕ производная^[k] p равна сумме по опоре: derivative^[k] p = ∑_{x ∈ supp(derivative^[k] p)} C((x+k).descFactorial k • p.coeff(x+k)) · X^x.
LaTeX
$$$$ \operatorname{derivative}^{k} p = \sum_{x \in (\operatorname{derivative}^{k} p).\operatorname{support}} C((x + k).descFactorial k \cdot p.\operatorname{coeff}(x + k)) \cdot X^x $$$$
Lean4
theorem iterate_derivative_eq_sum (p : R[X]) (k : ℕ) :
derivative^[k] p = ∑ x ∈ (derivative^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x :=
by
conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]
refine sum_congr rfl fun i _ ↦ ?_
rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]
