English
For natural n, ContDiff 𝕜 n f is equivalent to ContDiff on cast-n with derivatives conditions for iteratedDeriv.
Русский
Для натурального n, ContDiff 𝕜 n f эквивалентно ContDiff при приведении к типу cast-n с условиями по iteratedDeriv.
LaTeX
$$$ContDiff\ 𝕜\ n\ f \iff \Bigl(\forall m:\nats{\mathbb N}, m \le n \Rightarrow Continuous(iteratedDeriv m f)\Bigr) \land \Bigl(\forall m:\nats{\mathbb N}, m < n \Rightarrow Differentiable 𝕜 (iteratedDeriv m f)\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_nat_iff_iteratedDeriv {n : ℕ} :
ContDiff 𝕜 n f ↔
(∀ m : ℕ, m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ m : ℕ, m < n → Differentiable 𝕜 (iteratedDeriv m f) :=
by
rw [← WithTop.coe_natCast, contDiff_iff_iteratedDeriv]
simp
