iterate_derivative_eq_factorial_smul_sum

English

For p ∈ R[X] and k ∈ ℕ, the k-th derivative of p is k! times the sum over the support of the k-th derivative of p of C((x+k).choose k • p.coeff(x+k)) · X^x:

Русский

Для p ∈ R[X] и k ∈ ℕ k-й производной p равна k! умножить на сумму по опоре derivate^k(p): C((x+k).choose k • p.coeff(x+k)) · X^x.

LaTeX

$$$$ \operatorname{derivative}^{k} p = k! \cdot \sum_{x \in (\operatorname{derivative}^{k} p).\operatorname{support}} C((x + k).choose k \cdot p.\operatorname{coeff}(x + k)) \cdot X^x $$$$

Lean4

theorem iterate_derivative_eq_factorial_smul_sum (p : R[X]) (k : ℕ) :
    derivative^[k] p = k ! • ∑ x ∈ (derivative^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x :=
  by
  conv_lhs => rw [iterate_derivative_eq_sum]
  rw [smul_sum]
  refine sum_congr rfl fun i _ ↦ ?_
  rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]

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