# Higher differentiability in finite dimensions. #

### Finite dimensional results #

theorem contDiffOn_clm_apply {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] [] {n : ℕ∞} {f : EF →L[𝕜] G} {s : Set E} [] :
ContDiffOn 𝕜 n f s ∀ (y : F), ContDiffOn 𝕜 n (fun (x : E) => (f x) y) s

A family of continuous linear maps is C^n on s if all its applications are.

theorem contDiff_clm_apply_iff {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] [] {n : ℕ∞} {f : EF →L[𝕜] G} [] :
ContDiff 𝕜 n f ∀ (y : F), ContDiff 𝕜 n fun (x : E) => (f x) y
theorem contDiff_succ_iff_fderiv_apply {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] [] [] {n : } {f : EF} :
ContDiff 𝕜 (↑(n + 1)) f ∀ (y : E), ContDiff 𝕜 n fun (x : E) => (fderiv 𝕜 f x) y

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 (E and F). 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 E.

theorem contDiffOn_succ_of_fderiv_apply {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] [] [] {n : } {f : EF} {s : Set E} (hf : ) (h : ∀ (y : E), ContDiffOn 𝕜 (↑n) (fun (x : E) => (fderivWithin 𝕜 f s x) y) s) :
ContDiffOn 𝕜 (↑(n + 1)) f s
theorem contDiffOn_succ_iff_fderiv_apply {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] [] [] {n : } {f : EF} {s : Set E} (hs : ) :
ContDiffOn 𝕜 (↑(n + 1)) f s ∀ (y : E), ContDiffOn 𝕜 (↑n) (fun (x : E) => (fderivWithin 𝕜 f s x) y) s