English
On a set with unique differentiability, HasFTaylorSeriesUpToOn n f p s equates the Taylor coefficient to the iterated derivative inside the set, for all m ≤ n and x ∈ s.
Русский
На множестве с уникальной дифференцируемостью HasFTaylorSeriesUpToOn n f p s равенству коэффициента Тейлора и iteratedFDerivWithin на s при m ≤ n и x ∈ s.
LaTeX
$$$\text{HasFTaylorSeriesUpToOn } n f p s \to (\forall {m}, m \le n \to UniqueDiffOn 𝕜 s \to x \in s \to p x m = iteratedFDerivWithin 𝕜 m f s x)$$$
Lean4
theorem add {n : WithTop ℕ∞} {q g} (hf : HasFTaylorSeriesUpToOn n f p s) (hg : HasFTaylorSeriesUpToOn n g q s) :
HasFTaylorSeriesUpToOn n (f + g) (p + q) s := by
exact
HasFTaylorSeriesUpToOn.continuousLinearMap_comp (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F)
(hf.prodMk hg)
-- The sum is smooth.
