Higher differentiability in finite dimensions.

Finite-dimensional results

theorem contDiffWithinAt_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f : D → E →L[𝕜] F} {s : Set D} {x : D} [FiniteDimensional 𝕜 E] : ContDiffWithinAt 𝕜 n f s x ↔ ∀ (y : E), ContDiffWithinAt 𝕜 n (fun (x : D) => (f x) y) s x

A family of continuous linear maps is C^n at x within s if and only if all its applications are.

theorem contDiffOn_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f : D → E →L[𝕜] F} {s : Set D} [FiniteDimensional 𝕜 E] : ContDiffOn 𝕜 n f s ↔ ∀ (y : E), ContDiffOn 𝕜 n (fun (x : D) => (f x) y) s

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

theorem contDiff_clm_apply_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f : D → E →L[𝕜] F} [FiniteDimensional 𝕜 E] : ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff 𝕜 n fun (x : D) => (f x) y

theorem contDiff_succ_iff_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {f : D → E} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 D] : ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ⊤ → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ (y : D), ContDiff 𝕜 n fun (x : D) => (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 (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 contDiffOn_succ_of_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {f : D → E} {s : Set D} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 D] (hf : DifferentiableOn 𝕜 f s) (h'f : n = ⊤ → AnalyticOn 𝕜 f s) (h : ∀ (y : D), ContDiffOn 𝕜 n (fun (x : D) => (fderivWithin 𝕜 f s x) y) s) : ContDiffOn 𝕜 (n + 1) f s

theorem contDiffOn_succ_iff_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {f : D → E} {s : Set D} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 D] (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ∀ (y : D), ContDiffOn 𝕜 n (fun (x : D) => (fderivWithin 𝕜 f s x) y) s