English
If for every m, (m ≤ n) implies ContinuousOn (iteratedDerivWithin m f s) on s, and for every m, (m < n) implies DifferentiableOn (iteratedDerivWithin m f s) on s, then ContDiffOn 𝕜 n f s.
Русский
Если для каждого m верно, что m ≤ n тогда (iteratedDerivWithin m f s) непрерывна на s, и для каждого m верно, что m < n тогда (iteratedDerivWithin m f s) дифференцируема на s, то f ∈ ContDiffOn 𝕜 n f s.
LaTeX
$$$\biggl(\forall m:\nats{\mathbb N},\ (m:\nats{\mathbb N}_\infty) \le n \Rightarrow ContinuousOn(\iteratedDerivWithin\ m\ f\ s)\ s\biggr) \land \biggl(\forall m:\nats{\mathbb N},\ (m:\nats{\mathbb N}_\infty) < n \Rightarrow DifferentiableOn\ 𝕜\ (\iteratedDerivWithin\ m\ f\ s)\ s\biggr) \Longrightarrow\ ContDiffOn 𝕜 n f s$$
Lean4
/-- If the first `n` derivatives within a set of a function are continuous, and its first `n-1`
derivatives are differentiable, then the function is `C^n`. This is not an equivalence in general,
but this is an equivalence when the set has unique derivatives, see
`contDiffOn_iff_continuousOn_differentiableOn_deriv`. -/
theorem contDiffOn_of_continuousOn_differentiableOn_deriv {n : ℕ∞}
(Hcont : ∀ m : ℕ, (m : ℕ∞) ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s)
(Hdiff : ∀ m : ℕ, (m : ℕ∞) < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s) :
ContDiffOn 𝕜 n f s := by
apply contDiffOn_of_continuousOn_differentiableOn
· simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff]
· simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]
