English
If f = O[𝓝[s] x0] of its distance to x0 with exponent n > 1, and x0 ∈ s, then f has a Frechet derivative 0 within s at x0.
Русский
Пусть f удовлетворяет условию f = O[𝓝[s] x0] на расстоянии к x0 с показателем n > 1, при этом x0 ∈ s. Тогда у f существует внутри s в точке x0 производная Фреше, равная 0.
LaTeX
$$$(\exists h : f =O[𝓝[s] x₀] \big(\lambda x, \|x- x₀\|^n\big)) \land x₀ \in s \land 1 < n \implies HasFDerivWithinAt f (0 : E →L[𝕜] F) s x₀$$$
Lean4
theorem hasFDerivWithinAt {s : Set E} {x₀ : E} {n : ℕ} (h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s)
(hn : 1 < n) : HasFDerivWithinAt f (0 : E →L[𝕜] F) s x₀ := by
simp_rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO, h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply,
sub_zero, h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]
