differentiableWithinAt_iteratedDerivWithin

English

If f is ContDiffWithinAt 𝕜 n f s x, m < n, and insert x s has unique derivatives, then DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x.

Русский

Если f ∈ ContDiffWithinAt 𝕜 n f s x, и m < n, и у множества insert x s есть уникальные производные, тогда iteratedDerivWithin m f s дифференцируема внутри s в x.

LaTeX

$$$ContDiffWithinAt\ 𝕜\ n\ f\ s\ x \land m < n \land hs : UniqueDiffOn 𝕜 (insert x s) \Rightarrow DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x$$$

Lean4

theorem differentiableWithinAt_iteratedDerivWithin {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffWithinAt 𝕜 n f s x)
    (hmn : m < n) (hs : UniqueDiffOn 𝕜 (insert x s)) : DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x := by
  simpa only [iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableWithinAt_iff] using
    h.differentiableWithinAt_iteratedFDerivWithin hmn hs

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