hasFDerivAt — Mathlib

English

If f = O[𝓝 x₀] of the order ‖x−x₀‖^n (n>1) near x₀, then f has derivative 0 at x₀ in the usual sense.

Русский

Если f = O[𝓝 x₀] порядка ‖x−x₀‖^n (n>1) возле x₀, то в точке x₀ функция имеет производную 0 в обычном смысле.

LaTeX

$$$(f =O[𝓝 x₀] \|x- x₀\|^n) \land 1 < n \Rightarrow HasFDerivAt f (0 : E →L[𝕜] F) x₀$$$

Lean4

theorem hasFDerivAt {x₀ : E} {n : ℕ} (h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n) (hn : 1 < n) :
    HasFDerivAt f (0 : E →L[𝕜] F) x₀ := by
  rw [← nhdsWithin_univ] at h
  exact (h.hasFDerivWithinAt (mem_univ _) hn).hasFDerivAt_of_univ

Похожие утверждения