English
If a function has a derivative within a ball around x, then at points x+y with y in the ball, the derivative within is given by the first coefficient of p after a shift by y.
Русский
Если функция имеет производную внутри шара вокруг x, то в точках x+y с y внутри шара, производная внутри описана первым коэффициентом p после сдвига на y.
LaTeX
$$$\\text{HasFPowerSeriesWithinOnBall } f p s x r \\Rightarrow \\HasFDerivWithinAt f (\\ldots) (insert x s) (x+y)$$$
Lean4
theorem hasFDerivWithinAt [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r)
(h'y : x + y ∈ insert x s) :
HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1)) (insert x s) (x + y) :=
by
rcases eq_or_ne y 0 with rfl | h''y
· convert (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt
simp
· have Z := (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt
apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin
rw [nhdsWithin_insert_of_ne]
· exact self_mem_nhdsWithin
· simpa using h''y
