# mathlib3documentation

analysis.calculus.fderiv.restrict_scalars

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_strict_fderiv_at.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {f' : E →L[𝕜'] F} {x : E} (h : x) :
theorem has_fderiv_at_filter.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {f' : E →L[𝕜'] F} {x : E} {L : filter E} (h : x L) :
theorem has_fderiv_at.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {f' : E →L[𝕜'] F} {x : E} (h : f' x) :
theorem has_fderiv_within_at.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {f' : E →L[𝕜'] F} {s : set E} {x : E} (h : s x) :
theorem differentiable_at.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {x : E} (h : x) :
x
theorem differentiable_within_at.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {s : set E} {x : E} (h : s x) :
x
theorem differentiable_on.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {s : set E} (h : s) :
s
theorem differentiable.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} (h : f) :
theorem has_fderiv_within_at_of_restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {f' : E →L[𝕜'] F} {s : set E} {x : E} {g' : E →L[𝕜] F} (h : s x) (H : = g') :
s x
theorem has_fderiv_at_of_restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {f' : E →L[𝕜'] F} {x : E} {g' : E →L[𝕜] F} (h : g' x) (H : = g') :
f' x
theorem differentiable_at.fderiv_restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {x : E} (h : x) :
f x = (fderiv 𝕜' f x)
theorem differentiable_within_at_iff_restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {s : set E} {x : E} (hf : x) (hs : x) :
s x (g' : E →L[𝕜'] F), = s x
theorem differentiable_at_iff_restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} [ 𝕜'] {E : Type u_3} [ E] [ E] [ 𝕜' E] {F : Type u_4} [ F] [ F] [ 𝕜' F] {f : E F} {x : E} (hf : x) :
x (g' : E →L[𝕜'] F),