English
The HasFPowerSeriesWithinAt implies the HasFDerivWithinAt with the derivative given by the curry of the series at insert x s.
Русский
HasFPowerSeriesWithinAt влечёт HasFDerivWithinAt с производной, заданной карри-образованием плеянного ряда в insert x s.
LaTeX
$$$\text{HasFPowerSeriesWithinAt}(f,p,s,x) \Rightarrow \text{HasFDerivWithinAt}(f,\text{continuousMultilinearCurryFin1}(p))(\text{insert } x s, x)$$$
Lean4
theorem hasFDerivWithinAt (h : HasFPowerSeriesWithinAt f p s x) :
HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) (insert x s) x :=
by
rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO, isLittleO_iff]
intro c hc
have : Tendsto (fun y ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x)) :=
by
rw [nhdsWithin_prod_eq]
exact Tendsto.prodMk tendsto_id (tendsto_const_nhdsWithin (by simp))
exact this (isLittleO_iff.1 h.hasStrictFDerivWithinAt hc)
