mathlib3 documentation

analysis.calculus.deriv.linear

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) :
@[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) :
@[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) :
@[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) :
@[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) :
deriv e x = e 1
@[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) :

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) :
@[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) :
@[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) :
@[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) :
@[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) :
deriv e x = e 1
@[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) :