Restricting Scalars in Iterated Fréchet Derivatives

This file establishes standard theorems on restriction of scalars for iterated Fréchet derivatives, comparing iterated derivatives with respect to a field 𝕜' to iterated derivatives with respect to a subfield 𝕜 ⊆ 𝕜'. The results are analogous to those found in Mathlib.Analysis.Calculus.FDeriv.RestrictScalars.

theorem fderivWithin_restrictScalars_comp {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {x : E} {n : ℕ} {s : Set E} {φ : E → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) => E) F} (h : DifferentiableWithinAt 𝕜' φ s x) (hs : UniqueDiffWithinAt 𝕜 s x) : ⇑(fderivWithin 𝕜 (ContinuousMultilinearMap.restrictScalars 𝕜 ∘ φ) s x) = ContinuousMultilinearMap.restrictScalars 𝕜 ∘ ⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x))

Derivation rule for compositions of scalar restriction with continuous multilinear maps.

theorem ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {x : E} {f : E → F} {n : ℕ} {s : Set E} (h : ContDiffWithinAt 𝕜' (↑n) f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : ContinuousMultilinearMap.restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[nhdsWithin x s] iteratedFDerivWithin 𝕜 n f s

If f is n times continuously differentiable at x within s, then the nth iterated Fréchet derivative within s with respect to 𝕜 equals scalar restriction of the nth iterated Fréchet derivative within s with respect to 𝕜'.

theorem ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {x : E} {f : E → F} {n : ℕ} (h : ContDiffAt 𝕜' (↑n) f x) : ContinuousMultilinearMap.restrictScalars 𝕜 ∘ iteratedFDeriv 𝕜' n f =ᶠ[nhds x] iteratedFDeriv 𝕜 n f

If f is n times continuously differentiable at x, then the nth iterated Fréchet derivative with respect to 𝕜 equals scalar restriction of the nth iterated Fréchet derivative with respect to 𝕜'.

theorem ContDiffAt.restrictScalars_iteratedFDeriv {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {x : E} {f : E → F} {n : ℕ} (h : ContDiffAt 𝕜' (↑n) f x) : (ContinuousMultilinearMap.restrictScalars 𝕜 ∘ iteratedFDeriv 𝕜' n f) x = iteratedFDeriv 𝕜 n f x

If f is n times continuously differentiable at x, then the nth iterated Fréchet derivative with respect to 𝕜 equals scalar restriction of the nth iterated Fréchet derivative with respect to 𝕜'.