English
For natural n, ContDiffOn 𝕜 n f s is equivalent to having all m ≤ n continuous iterated derivatives and all m < n differentiable iterated derivatives.
Русский
Для натурального n равносильно тому, что все m ≤ n итеративные производные непрерывны и все m < n дифференцируемы.
LaTeX
$$$\text{ContDiffOn } 𝕜\ n\ f\ s \iff \Bigl(\forall m:\nats{\mathbb N}, (m:\nats{\mathbb N}) \le n \Rightarrow ContinuousOn(\ iteratedDerivWithin m f s) s\Bigr) \land \Bigl(\forall m:\nats{\mathbb N}, (m:\nats{\mathbb N}) < n \Rightarrow DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s\Bigr)$$$
Lean4
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
reformulated in terms of the one-dimensional derivative. -/
theorem contDiff_iff_iteratedDeriv {n : ℕ∞} :
ContDiff 𝕜 n f ↔
(∀ m : ℕ, (m : ℕ∞) ≤ n → Continuous (iteratedDeriv m f)) ∧
∀ m : ℕ, (m : ℕ∞) < n → Differentiable 𝕜 (iteratedDeriv m f) :=
by
simp only [contDiff_iff_continuous_differentiable, iteratedFDeriv_eq_equiv_comp,
LinearIsometryEquiv.comp_continuous_iff, LinearIsometryEquiv.comp_differentiable_iff]
