differentiableAt_iteratedFDeriv — Mathlib

English

If f is C^n at x and m < n, then the m-th iterated derivative map is differentiable at x.

Русский

Если функция f является C^n в точке x и m < n, то m-ая итеративная производная дифференцируема в точке x.

LaTeX

$$$ContDiffAt\ 𝕜\ n\ f\ x\ ∧ \uparrow m < n\Rightarrow DifferentiableAt\ 𝕜\ (iteratedFDeriv\ 𝕜\ m\ f)\ x$$$

Lean4

theorem differentiableAt_iteratedFDeriv {f : E → F} {n : WithTop ℕ∞} {m : ℕ} {x : E} (h : ContDiffAt 𝕜 n f x)
    (hmn : ↑m < n) : DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 m f) x :=
  by
  rw [← differentiableWithinAt_univ]
  convert (h.differentiableWithinAt_iteratedFDerivWithin hmn (by simp [uniqueDiffOn_univ]))
  exact iteratedFDerivWithin_univ.symm

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