contDiffOn_clm_apply
theorem contDiffOn_clm_apply :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
[inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : CompleteSpace 𝕜] {n : ℕ∞} {f : E → F →L[𝕜] G}
{s : Set E} [inst_8 : FiniteDimensional 𝕜 F],
ContDiffOn 𝕜 n f s ↔ ∀ (y : F), ContDiffOn 𝕜 n (fun x => (f x) y) s
The theorem `contDiffOn_clm_apply` states that for a given non-trivially normed field `𝕜`, normed additive commutative groups `E`, `F`, and `G`, and a set `s` which is a subset of `E`, a family of continuous linear maps `f` from `E` to `F →L[𝕜] G` is continuous differentiable on `s` up to order `n` if and only if all its applications, i.e., `(f x) y` for all `y` in `F`, are also continuously differentiable on `s` up to order `n`. Here, `F` is assumed to be finite-dimensional over `𝕜`, and `𝕜` is complete, meaning every Cauchy sequence of elements in `𝕜` has a limit in `𝕜`. This theorem ties the differentiability of the family of maps to the differentiability of each of its applications.
More concisely: A family of continuous linear maps from a non-trivially normed field into the finite-dimensional normed additive commutative group over the field is continuously differentiable on a subset up to order n if and only if each of its applications is continuously differentiable on that subset up to order n.
|
contDiff_succ_iff_fderiv_apply
theorem contDiff_succ_iff_fderiv_apply :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
[inst_5 : CompleteSpace 𝕜] [inst_6 : FiniteDimensional 𝕜 E] {n : ℕ} {f : E → F},
ContDiff 𝕜 (↑(n + 1)) f ↔ Differentiable 𝕜 f ∧ ∀ (y : E), ContDiff 𝕜 ↑n fun x => (fderiv 𝕜 f x) y
This theorem provides a useful characterization for determining whether a function is of class `C^(n+1)`, which is especially handy during an induction on `n`. It states that for any function `f` from `E` to `F`, where `E` is a finite-dimensional space over a non-trivially normed field `𝕜`, the function `f` is `C^(n+1)` continuously differentiable if and only if `f` is differentiable and for all `y` in `E`, the `n`-th derivative of `f` at `x` applied to `y` is continuously differentiable. One advantage of this version of the theorem over `contDiff_succ_iff_fderiv` is that both occurrences of `ContDiff` are for functions with the same domain and codomain (`E` and `F`), which avoids some complications related to generalizing `F` and universe issues.
More concisely: A function `f` from a finite-dimensional space `E` over a non-trivially normed field to another space `F` is `C^(n+1)` continuously differentiable if and only if it is differentiable and its `n`-th derivative is continuously differentiable.
|