Higher differentiability in finite dimensions. #
Finite dimensional results #
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]
:
A family of continuous linear maps is C^n on s 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]
:
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]
:
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