English
For natural n, ContDiff 𝕜 n f is equivalent to the conjunction of: (i) for all m ≤ n, x ↦ iteratedFDeriv 𝕜 m f x is continuous; and (ii) for all m < n, x ↦ iteratedFDeriv 𝕜 m f x is differentiable.
Русский
Для натурального n, ContDiff 𝕜 n f эквивалентно сочетанию: (i) для всех m ≤ n функция x ↦ iteratedFDeriv m f x непрерывна; (ii) для всех m < n функция x ↦ iteratedFDeriv m f x дифференцируема.
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}}\ n\ f \iff \Big(\forall m : \mathbb{N}, m \le n \Rightarrow \operatorname{Continuous}\ (x \mapsto \operatorname{iteratedFDeriv}_{\mathbb{K}}\ m\ f\ x)\Big) \land \Big(\forall m : \mathbb{N}, m < n \Rightarrow \operatorname{Differentiable}_{\mathbb{K}} (\operatorname{iteratedFDeriv}_{\mathbb{K}}\ m\ f)\Big)$$
Lean4
/-- If `f` is `C^n` then its `m`-times iterated derivative is differentiable for `m < n`. -/
theorem differentiable_iteratedFDeriv {m : ℕ} (hm : m < n) (hf : ContDiff 𝕜 n f) :
Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x :=
(contDiff_iff_continuous_differentiable.mp (hf.of_le (ENat.add_one_natCast_le_withTop_of_lt hm))).2 m
(mod_cast lt_add_one m)
