Derivatives of continuous linear maps from the base field #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that f : 𝕜 →L[𝕜] E (or f : 𝕜 →ₗ[𝕜] E) has derivative f 1.
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
analysis/calculus/deriv/basic.
Keywords #
derivative, linear map
Derivative of continuous linear maps #
@[protected]
theorem
continuous_linear_map.has_deriv_at_filter
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{L : filter 𝕜}
(e : 𝕜 →L[𝕜] F) :
has_deriv_at_filter ⇑e (⇑e 1) x L
@[protected]
theorem
continuous_linear_map.has_strict_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
(e : 𝕜 →L[𝕜] F) :
has_strict_deriv_at ⇑e (⇑e 1) x
@[protected]
theorem
continuous_linear_map.has_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
(e : 𝕜 →L[𝕜] F) :
has_deriv_at ⇑e (⇑e 1) x
@[protected]
theorem
continuous_linear_map.has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
(e : 𝕜 →L[𝕜] F) :
has_deriv_within_at ⇑e (⇑e 1) s x
@[protected, simp]
theorem
continuous_linear_map.deriv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
(e : 𝕜 →L[𝕜] F) :
@[protected]
theorem
continuous_linear_map.deriv_within
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
(e : 𝕜 →L[𝕜] F)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within ⇑e s x = ⇑e 1
Derivative of bundled linear maps #
@[protected]
theorem
linear_map.has_deriv_at_filter
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{L : filter 𝕜}
(e : 𝕜 →ₗ[𝕜] F) :
has_deriv_at_filter ⇑e (⇑e 1) x L
@[protected]
theorem
linear_map.has_strict_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
(e : 𝕜 →ₗ[𝕜] F) :
has_strict_deriv_at ⇑e (⇑e 1) x
@[protected]
theorem
linear_map.has_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
(e : 𝕜 →ₗ[𝕜] F) :
has_deriv_at ⇑e (⇑e 1) x
@[protected]
theorem
linear_map.has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
(e : 𝕜 →ₗ[𝕜] F) :
has_deriv_within_at ⇑e (⇑e 1) s x
@[protected, simp]
theorem
linear_map.deriv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
(e : 𝕜 →ₗ[𝕜] F) :
@[protected]
theorem
linear_map.deriv_within
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
(e : 𝕜 →ₗ[𝕜] F)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within ⇑e s x = ⇑e 1