Theorems · Theorem · real analysis

contDiffOn_of_differentiableOn_deriv

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞},
  (∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) → ContDiffOn 𝕜 (↑n) f s

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).

Defined in

Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Cited by

1 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace