differentiableOn_iteratedDerivWithin

English

If ContDiffOn 𝕜 n f s and m ≤ n, then DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s, assuming unique derivatives on s.

Русский

Если f ∈ ContDiffOn 𝕜 n f s и m ≤ n, то DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s, при условии уникальности производных на s.

LaTeX

$$$ContDiffOn\ 𝕜 n\ f\ s \land m ≤ n \land hs : UniqueDiffOn 𝕜 s \Rightarrow DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s$$$

Lean4

/-- On a set with unique derivatives, a `C^n` function has derivatives less than `n` which are
differentiable. -/
theorem differentiableOn_iteratedDerivWithin {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffOn 𝕜 n f s) (hmn : m < n)
    (hs : UniqueDiffOn 𝕜 s) : DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s := fun x hx =>
  (h x hx).differentiableWithinAt_iteratedDerivWithin hmn <| by rwa [insert_eq_of_mem hx]

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