English
In general HasFTaylorSeriesUpToOn implies HasStrictFDerivAt for n≥1 with interior neighborhood condition.
Русский
В общем HasFTaylorSeriesUpToOn влечёт HasStrictFDerivAt для n≥1 при условии внутри области определения.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn } n f p s \Rightarrow \text{HasStrictFDerivAt } f (p x 1) x.$$$$
Lean4
/-- If a function is `C^n` with `1 ≤ n` around a point, and its derivative at that point is given to
us as `f'`, then `f'` is also a strict derivative. -/
theorem hasStrictFDerivAt' {f : E' → F'} {f' : E' →L[𝕂] F'} {x : E'} (hf : ContDiffAt 𝕂 n f x)
(hf' : HasFDerivAt f f' x) (hn : 1 ≤ n) : HasStrictFDerivAt f f' x :=
by
rcases hf.of_le hn 1 le_rfl with ⟨u, H, p, hp⟩
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem] at H
have := hp.hasStrictFDerivAt le_rfl H
rwa [hf'.unique this.hasFDerivAt]
