English
If HasFTaylorSeriesUpTo n f p holds with hn: 1 ≤ n, then f is differentiable at every x, and its derivative is given by the first nonzero coefficient, namely HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x.
Русский
Если f имеет ряд Тейлора до порядка n≥1, то f дифференцируема в каждой точке x, и её производная равна соответствующему коэффициенту первого порядка: HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x.
LaTeX
$$$\\text{HasFTaylorSeriesUpTo } n f p \\;\\Rightarrow\\; \\forall x, \\text{HasFDerivAt } f (\\operatorname{continuousMultilinearCurryFin1}_{𝕜 E F} (p x 1))\, x$$
Lean4
/-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
series is a derivative of `f`. -/
theorem hasFDerivAt (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) (x : E) :
HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x :=
by
rw [← hasFDerivWithinAt_univ]
exact (hasFTaylorSeriesUpToOn_univ_iff.2 h).hasFDerivWithinAt hn (mem_univ _)
