English
For natural n, HasFTaylorSeriesUpToOn (n+1) f p s is equivalent to HasFTaylorSeriesUpToOn n f p s, plus a derivative condition for p at order n, and continuity of p at order n+1.
Русский
Для натурального n, HasFTaylorSeriesUpToOn (n+1) f p s эквивалентно HasFTaylorSeriesUpToOn n f p s, плюс условие производной для p на порядке n и непрерывность на порядке n+1.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(n+1,f,p,s) \iff \text{HasFTaylorSeriesUpToOn}(n,f,p,s) \land \Big( \forall x\in s, \text{HasFDerivWithinAt}(f, p x n, s, x) \Big) \land \text{ContinuousOn}(p(\cdot)(n+1), s). $$$$
Lean4
/-- If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then
in a neighborhood of `x`, the term of order `1` of this series is a derivative of `f`. -/
theorem eventually_hasFDerivAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) :
∀ᶠ y in 𝓝 x, HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p y 1)) y :=
(eventually_eventually_nhds.2 hx).mono fun _y hy => h.hasFDerivAt hn hy
