iterate_derivative_sum — Mathlib

English

For any natural k, the kth iterate of the derivative operator commutes with finite sums: the kth derivative of the sum over b in s of f(b) equals the sum over b in s of the kth derivative of f(b).

Русский

Для любого натурального k кратная итерация оператора производной коммутирует с конечной суммой: k-я производная от суммы по b∈s f(b) равна сумме k-й производной от f(b).

LaTeX

$$$\operatorname{derivative}^{k}\left(\sum_{b \in s} f(b)\right) = \sum_{b \in s} \operatorname{derivative}^{k}\left(f(b)\right)$$$

Lean4

theorem iterate_derivative_sum (k : ℕ) (s : Finset ι) (f : ι → R[X]) :
    derivative^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, derivative^[k] (f b) := by simp_rw [← Module.End.pow_apply, map_sum]

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