The derivative of bounded linear maps #
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 bounded linear maps.
Continuous linear maps #
There are currently two variants of these in mathlib, the bundled version
(named continuous_linear_map, and denoted E →L[𝕜] F), and the unbundled version (with a
predicate is_bounded_linear_map). We give statements for both versions.
@[protected]
theorem
continuous_linear_map.has_strict_fderiv_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E} :
has_strict_fderiv_at ⇑e e x
@[protected]
theorem
continuous_linear_map.has_fderiv_at_filter
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E}
{L : filter E} :
has_fderiv_at_filter ⇑e e x L
@[protected]
theorem
continuous_linear_map.has_fderiv_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E}
{s : set E} :
has_fderiv_within_at ⇑e e s x
@[protected]
theorem
continuous_linear_map.has_fderiv_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E} :
has_fderiv_at ⇑e e x
@[protected, simp]
theorem
continuous_linear_map.differentiable_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E} :
differentiable_at 𝕜 ⇑e x
@[protected]
theorem
continuous_linear_map.differentiable_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E}
{s : set E} :
differentiable_within_at 𝕜 ⇑e s x
@[protected, simp]
theorem
continuous_linear_map.fderiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E} :
@[protected]
theorem
continuous_linear_map.fderiv_within
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{x : E}
{s : set E}
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 ⇑e s x = e
@[protected, simp]
theorem
continuous_linear_map.differentiable
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F) :
differentiable 𝕜 ⇑e
@[protected]
theorem
continuous_linear_map.differentiable_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e : E →L[𝕜] F)
{s : set E} :
differentiable_on 𝕜 ⇑e s
theorem
is_bounded_linear_map.has_fderiv_at_filter
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{L : filter E}
(h : is_bounded_linear_map 𝕜 f) :
theorem
is_bounded_linear_map.has_fderiv_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{s : set E}
(h : is_bounded_linear_map 𝕜 f) :
theorem
is_bounded_linear_map.has_fderiv_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
(h : is_bounded_linear_map 𝕜 f) :
theorem
is_bounded_linear_map.differentiable_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
(h : is_bounded_linear_map 𝕜 f) :
differentiable_at 𝕜 f x
theorem
is_bounded_linear_map.differentiable_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{s : set E}
(h : is_bounded_linear_map 𝕜 f) :
differentiable_within_at 𝕜 f s x
theorem
is_bounded_linear_map.fderiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
(h : is_bounded_linear_map 𝕜 f) :
fderiv 𝕜 f x = h.to_continuous_linear_map
theorem
is_bounded_linear_map.fderiv_within
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{s : set E}
(h : is_bounded_linear_map 𝕜 f)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 f s x = h.to_continuous_linear_map
theorem
is_bounded_linear_map.differentiable
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(h : is_bounded_linear_map 𝕜 f) :
differentiable 𝕜 f
theorem
is_bounded_linear_map.differentiable_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{s : set E}
(h : is_bounded_linear_map 𝕜 f) :
differentiable_on 𝕜 f s