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) :
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) :
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) :
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) :
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') :
has_fderiv_within_at f f' s x
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') :
has_fderiv_at f f' x
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) :
fderiv 𝕜 f x = continuous_linear_map.restrict_scalars 𝕜 (fderiv 𝕜' 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) :
differentiable_within_at 𝕜' f s x ↔ ∃ (g' : E →L[𝕜'] F), continuous_linear_map.restrict_scalars 𝕜 g' = fderiv_within 𝕜 f 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) :
differentiable_at 𝕜' f x ↔ ∃ (g' : E →L[𝕜'] F), continuous_linear_map.restrict_scalars 𝕜 g' = fderiv 𝕜 f x