English
For hf and hg expressing ContDiffWithinAt, the nth iterated derivative of f + g within s at x equals the sum of the nth iterated derivatives of f and g within s at x.
Русский
Для hf и hg, задающих ContDiffWithinAt, n-я повторная производная внутри s функции f+g в точке x равна сумме n-й повторной производной f и n-й повторной производной g внутри s в точке x.
LaTeX
$$$\\operatorname{iteratedDerivWithin}_n (f+g)\\ s\\ x = \\operatorname{iteratedDerivWithin}_n f\\ s\\ x + \\operatorname{iteratedDerivWithin}_n g\\ s\\ x$$
Lean4
theorem iteratedDerivWithin_add (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x := by
simp_rw [iteratedDerivWithin, iteratedFDerivWithin_add_apply hf hg h hx, ContinuousMultilinearMap.add_apply]
