English
The i-th iterated derivative of a finite sum equals the sum of i-th iterated derivatives.
Русский
i-я итеративная производная суммы равна сумме i-й производной каждого слагаемого.
LaTeX
$$$\operatorname{iteratedFDeriv}_{\mathbb{K}} i (\sum j ∈ u, f_j ·) = \sum j ∈ u, \operatorname{iteratedFDeriv}_{\mathbb{K}} i (f_j)$$$
Lean4
theorem iteratedFDerivWithin_sum_apply {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E}
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 i (f j) s x) :
iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j ·) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x := by
induction u using Finset.cons_induction with
| empty => simp
| cons a u ha IH =>
simp only [Finset.mem_cons, forall_eq_or_imp] at h
simp only [Finset.sum_cons]
rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
