English
Let i be a natural number and f, g be functions with i-th order differentiability at x. Then the i-th iterated derivative at x of f + g equals the sum of the i-th iterated derivatives: D^i(f+g)(x) = D^i f(x) + D^i g(x).
Русский
Пусть i — натуральное число, функции f и g удовлетворяют условию i-й производной в точке x. Тогда i-я итеративная производная от суммы равна сумме i-й производных: D^i(f+g)(x) = D^i f(x) + D^i g(x).
LaTeX
$$$\operatorname{iteratedFDeriv}_{\mathbb{K}} i (f+g)(x) = \operatorname{iteratedFDeriv}_{\mathbb{K}} i f(x) + \operatorname{iteratedFDeriv}_{\mathbb{K}} i g(x)$$$
Lean4
theorem iteratedFDeriv_add_apply' {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
iteratedFDeriv 𝕜 i (fun x => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x :=
iteratedFDeriv_add_apply hf hg
