English
If a function f has a Taylor series up to order n≥1 on a set s around x, then the term of order 1 in the series is the strict derivative at x.
Русский
Если функция f имеет ряд Тейлора до порядка n≥1 на области s вокруг x, тогда член порядка 1 ряда является строгим производным в точке x.
LaTeX
$$$$\text{If } hf: \text{HasFTaylorSeriesUpToOn } n f p s, \ n?≥1, \text{ then } HasStrictFDerivAt f ((p x) 1) x.$$$$
Lean4
/-- If a function has a Taylor series at order at least 1, then at points in the interior of the
domain of definition, the term of order 1 of this series is a strict derivative of `f`. -/
theorem hasStrictFDerivAt {n : WithTop ℕ∞} {s : Set E'} {f : E' → F'} {x : E'}
{p : E' → FormalMultilinearSeries 𝕂 E' F'} (hf : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hs : s ∈ 𝓝 x) :
HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x :=
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt (hf.eventually_hasFDerivAt hn hs) <|
(continuousMultilinearCurryFin1 𝕂 E' F').continuousAt.comp <| (hf.cont 1 hn).continuousAt hs
