English
If f is differentiable on s and fderivWithin behaves, then f is C^(n+1) on s given a suitable auxiliary condition.
Русский
Если f дифференцируема на s и fderivWithin удовлетворяет условию, тогда f ∈ C^(n+1) на s при подходящем условии.
LaTeX
$$contDiffOn_succ_of_fderiv_apply hf h'f h : ContDiffOn 𝕜 (n + 1) f s$$
Lean4
/-- This is a useful lemma to prove that a certain operation preserves functions being `C^n`.
When you do induction on `n`, this gives a useful characterization of a function being `C^(n+1)`,
assuming you have already computed the derivative. The advantage of this version over
`contDiff_succ_iff_fderiv` is that both occurrences of `ContDiff` are for functions with the same
domain and codomain (`D` and `E`). This is not the case for `contDiff_succ_iff_fderiv`, which
often requires an inconvenient need to generalize `F`, which results in universe issues
(see the discussion in the section of `ContDiff.comp`).
This lemma avoids these universe issues, but only applies for finite-dimensional `D`. -/
theorem contDiff_succ_iff_fderiv_apply [FiniteDimensional 𝕜 D] :
ContDiff 𝕜 (n + 1) f ↔
Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ y, ContDiff 𝕜 n fun x => fderiv 𝕜 f x y :=
by rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]
