English
If f admits a translated power-series expansion within s around x, then the corresponding Frechet derivative within (insert x s) at x holds.
Русский
Если функция f имеет разложение в ряд Фурье вокруг точки x внутри s, то соответствующая производнаяФреше внутри (insert x s) в точке x существует.
LaTeX
$$$\text{HasFDerivWithinAt}(f, p, s, x) \Rightarrow \text{HasFDerivWithinAt}(f, \text{continuousMultilinearCurrying}(p), \text{insert } x s, x)$$$
Lean4
/-- A function which is analytic within a set is strictly differentiable there. Since we
don't have a predicate `HasStrictFDerivWithinAt`, we spell out what it would mean. -/
theorem hasStrictFDerivWithinAt (h : HasFPowerSeriesWithinAt f p s x) :
(fun y ↦
f y.1 - f y.2 - (continuousMultilinearCurryFin1 𝕜 E F (p 1)) (y.1 - y.2)) =o[𝓝[insert x s ×ˢ insert x s] (x, x)]
fun y ↦ y.1 - y.2 :=
by
refine h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right ?_)
refine isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, ?_, EventuallyEq.rfl⟩
apply Tendsto.mono_left _ nhdsWithin_le_nhds
refine (continuous_id.sub continuous_const).norm.tendsto' _ _ ?_
rw [_root_.id, sub_self, norm_zero]
