mathlib3 documentation

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