differentiableOn_iteratedFDerivWithin

English

If AnalyticOn 𝕜 f s and UniqueDiffOn 𝕜 s, then ContDiffOn 𝕜 n f s.

Русский

Если AnalyticOn 𝕜 f s и UniqueDiffOn 𝕜 s, то ContDiffOn 𝕜 n f s.

LaTeX

$$$AnalyticOn\\ 𝕜\\ f\\ s \\rightarrow UniqueDiffOn\\ 𝕜\\ s \\rightarrow ContDiffOn\\ 𝕜\\ n\\ f\\ s$$$

Lean4

theorem differentiableOn_iteratedFDerivWithin {m : ℕ} (h : ContDiffOn 𝕜 n f s) (hmn : m < n) (hs : UniqueDiffOn 𝕜 s) :
    DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s :=
  by
  intro x hx
  have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hmn
  apply (((h.of_le this).ftaylorSeriesWithin hs).fderivWithin m ?_ x hx).differentiableWithinAt
  exact_mod_cast lt_add_one m

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