The derivative of the scalar restriction of a linear map

For detailed documentation of the Fréchet derivative, see the module docstring of Mathlib/Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of the scalar restriction of a linear map.

Restricting from ℂ to ℝ, or generally from 𝕜' to 𝕜

If a function is differentiable over ℂ, then it is differentiable over ℝ. In this paragraph, we give variants of this statement, in the general situation where ℂ and ℝ are replaced respectively by 𝕜' and 𝕜 where 𝕜' is a normed algebra over 𝕜.

theorem HasFDerivAtFilter.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {f' : E →L[𝕜'] F} {L : Filter (E × E)} (h : HasFDerivAtFilter f f' L) : HasFDerivAtFilter f (ContinuousLinearMap.restrictScalars 𝕜 f') L

theorem HasStrictFDerivAt.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {f' : E →L[𝕜'] F} {x : E} (h : HasStrictFDerivAt f f' x) : HasStrictFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x

theorem HasFDerivAt.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {f' : E →L[𝕜'] F} {x : E} (h : HasFDerivAt f f' x) : HasFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x

theorem HasFDerivWithinAt.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {f' : E →L[𝕜'] F} {s : Set E} {x : E} (h : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x

theorem DifferentiableAt.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {x : E} (h : DifferentiableAt 𝕜' f x) : DifferentiableAt 𝕜 f x

theorem DifferentiableWithinAt.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {s : Set E} {x : E} (h : DifferentiableWithinAt 𝕜' f s x) : DifferentiableWithinAt 𝕜 f s x

theorem DifferentiableOn.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {s : Set E} (h : DifferentiableOn 𝕜' f s) : DifferentiableOn 𝕜 f s

theorem Differentiable.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} (h : Differentiable 𝕜' f) : Differentiable 𝕜 f

theorem HasFDerivWithinAt.of_restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {f' : E →L[𝕜'] F} {s : Set E} {x : E} {g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x) (H : ContinuousLinearMap.restrictScalars 𝕜 f' = g') : HasFDerivWithinAt f f' s x

theorem hasFDerivAt_of_restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {f' : E →L[𝕜'] F} {x : E} {g' : E →L[𝕜] F} (h : HasFDerivAt f g' x) (H : ContinuousLinearMap.restrictScalars 𝕜 f' = g') : HasFDerivAt f f' x

theorem DifferentiableAt.fderiv_restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {x : E} (h : DifferentiableAt 𝕜' f x) : fderiv 𝕜 f x = ContinuousLinearMap.restrictScalars 𝕜 (fderiv 𝕜' f x)

theorem DifferentiableWithinAt.restrictScalars_fderivWithin (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {s : Set E} {x : E} (hf : DifferentiableWithinAt 𝕜' f s x) (hs : UniqueDiffWithinAt 𝕜 s x) : ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' f s x) = fderivWithin 𝕜 f s x

theorem differentiableWithinAt_iff_restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {s : Set E} {x : E} (hf : DifferentiableWithinAt 𝕜 f s x) (hs : UniqueDiffWithinAt 𝕜 s x) : DifferentiableWithinAt 𝕜' f s x ↔ ∃ (g' : E →L[𝕜'] F), ContinuousLinearMap.restrictScalars 𝕜 g' = fderivWithin 𝕜 f s x

theorem differentiableAt_iff_restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [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] {f : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜' f x ↔ ∃ (g' : E →L[𝕜'] F), ContinuousLinearMap.restrictScalars 𝕜 g' = fderiv 𝕜 f x