English
If for all i in u, DifferentiableWithinAt 𝕜 (A_i) s x holds, then derivWithin of the sum equals the sum of derivWithin of A_i.
Русский
Если для каждого i ∈ u функция A_i дифференцируема внутри s в x, то производная по derivWithin от суммы равна сумме производных derivWithin каждой A_i.
LaTeX
$$$\\forall i \\in u,\\ DifferentiableWithinAt 𝕜 (A_i) s x \\Rightarrow derivWithin(\\lambda y. \\sum_{i\\in u} A_i(y)) s x = \\sum_{i\\in u} derivWithin(A_i) s x.$$$
Lean4
theorem derivWithin_fun_sum (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
derivWithin (fun y ↦ ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (HasDerivWithinAt.fun_sum fun i hi ↦ (h i hi).hasDerivWithinAt).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
