English
If for all m, Differentiable 𝕜 (iteratedDeriv m f), then ContDiff 𝕜 n f.
Русский
Если все iteratedDeriv m f дифференцируемы, тогда f ∈ ContDiff 𝕜 n f.
LaTeX
$$(\forall m : Nat, (m : ℕ∞) ≤ n → Differentiable 𝕜 (iteratedDeriv m f)) → ContDiff 𝕜 (WithTop.some n) f$$
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 contDiff_of_differentiable_iteratedDeriv {n : ℕ∞}
(h : ∀ m : ℕ, (m : ℕ∞) ≤ n → Differentiable 𝕜 (iteratedDeriv m f)) : ContDiff 𝕜 n f :=
contDiff_iff_iteratedDeriv.2 ⟨fun m hm => (h m hm).continuous, fun m hm => h m (le_of_lt hm)⟩
