# The derivative of the scalar restriction of a linear map #

For detailed documentation of the FrΓ©chet derivative, see the module docstring of 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 HasStrictFDerivAt.restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} {f' : E βL[π'] F} {x : E} (h : ) :
theorem HasFDerivAtFilter.restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} {f' : E βL[π'] F} {x : E} {L : } (h : HasFDerivAtFilter f f' x L) :
theorem HasFDerivAt.restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} {f' : E βL[π'] F} {x : E} (h : HasFDerivAt f f' x) :
theorem HasFDerivWithinAt.restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} {f' : E βL[π'] F} {s : Set E} {x : E} (h : HasFDerivWithinAt f f' s x) :
theorem DifferentiableAt.restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} {x : E} (h : DifferentiableAt π' f x) :
DifferentiableAt π f x
theorem DifferentiableWithinAt.restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [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) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [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) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} (h : Differentiable π' f) :
Differentiable π f
theorem HasFDerivWithinAt.of_restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [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 : = g') :
theorem hasFDerivAt_of_restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [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 : = g') :
theorem DifferentiableAt.fderiv_restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [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_iff_restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [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), = fderivWithin π f s x
theorem differentiableAt_iff_restrictScalars (π : Type u_1) [] {π' : Type u_2} [] [NormedAlgebra π π'] {E : Type u_3} [NormedSpace π E] [NormedSpace π' E] [IsScalarTower π π' E] {F : Type u_4} [NormedSpace π F] [NormedSpace π' F] [IsScalarTower π π' F] {f : E β F} {x : E} (hf : DifferentiableAt π f x) :
DifferentiableAt π' f x β β (g' : E βL[π'] F), = fderiv π f x