English
Let 𝕜 be a field and E a normed space. If each function A_i is differentiable at x for i in a finite index set u, then the derivative at x of the sum ∑_{i ∈ u} A_i is the sum of their derivatives at x. In particular, D_x(∑_{i∈u} A_i) = ∑_{i∈u} DA_i(x).
Русский
Пусть 𝕜 — поле, E — нормированное пространство. Пусть для всех i в конечном множестве u функции A_i дифференцируемы в точке x; тогда производная в x от суммы ∑_{i∈u} A_i равна сумме производных: D_x(∑_{i∈u} A_i) = ∑_{i∈u} DA_i(x).
LaTeX
$$$\displaystyle fderiv\;\,\mathit{at}\;\,\,\(\,\,\text{of }\; y \mapsto \sum_{i \in u} A_i(y)\;\;\text{at } x = \sum_{i \in u} fderiv\;\,\mathit{at}\;\,\,\(\mathrm{A_i} \; x\) }$$$
Lean4
theorem fderiv_fun_sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) :
fderiv 𝕜 (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, fderiv 𝕜 (A i) x :=
(HasFDerivAt.fun_sum fun i hi => (h i hi).hasFDerivAt).fderiv
