English
If for every m, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) on s, then ContDiffOn 𝕜 n f s.
Русский
Если для каждого m функция iteratedDerivWithin m f s дифференцируема на s, то f ∈ ContDiffOn 𝕜 n f s.
LaTeX
$$$\bigl(\forall m:\nats{\mathbb N},\ (m:\nats{\mathbb N}) \le n \Rightarrow DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s\bigr) \Rightarrow ContDiffOn 𝕜 n f s$$
Lean4
/-- To check that a function is `n` times continuously differentiable, it suffices to check that its
first `n` derivatives are differentiable. This is slightly too strong as the condition we
require on the `n`-th derivative is differentiability instead of continuity, but it has the
advantage of avoiding the discussion of continuity in the proof (and for `n = ∞` this is optimal).
-/
theorem contDiffOn_of_differentiableOn_deriv {n : ℕ∞}
(h : ∀ m : ℕ, (m : ℕ∞) ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) : ContDiffOn 𝕜 n f s :=
by
apply contDiffOn_of_differentiableOn
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]
