English
The sum of two C^n functions is C^n.
Русский
Сумма двух функций класса C^n является C^n.
LaTeX
$$$\text{ContDiffOn 𝕜 n f} \land \text{ContDiffOn 𝕜 n g} \Rightarrow \text{ContDiff 𝕜 n (f+g)}$$$
Lean4
/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
See also `iteratedFDerivWithin_add_apply'`, which uses the spelling `(fun x ↦ f x + g x)`
instead of `f + g`. -/
theorem iteratedFDerivWithin_add_apply {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x) (hg : ContDiffWithinAt 𝕜 i g s x)
(hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x :=
by
have := (hf.eventually (by simp)).and (hg.eventually (by simp))
obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
have H : ↑(s ∩ t) =ᶠ[𝓝 x] s := inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H]
exact
.symm
(((hft.ftaylorSeriesWithin hut).add (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl
hut ⟨hx, hxt⟩)
