Documentation

Mathlib.Analysis.Calculus.Deriv.Linear

Derivatives of continuous linear maps from the base field #

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 #

theorem ContinuousLinearMap.hasDerivAtFilter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {L : Filter 𝕜} (e : 𝕜 →L[𝕜] F) :
HasDerivAtFilter (⇑e) (e 1) x L
theorem ContinuousLinearMap.hasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
HasStrictDerivAt (⇑e) (e 1) x
theorem ContinuousLinearMap.hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
HasDerivAt (⇑e) (e 1) x
theorem ContinuousLinearMap.hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →L[𝕜] F) :
HasDerivWithinAt (⇑e) (e 1) s x
@[simp]
theorem ContinuousLinearMap.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
deriv (⇑e) x = e 1
theorem ContinuousLinearMap.derivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →L[𝕜] F) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (⇑e) s x = e 1

Derivative of bundled linear maps #

theorem LinearMap.hasDerivAtFilter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {L : Filter 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasDerivAtFilter (⇑e) (e 1) x L
theorem LinearMap.hasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasStrictDerivAt (⇑e) (e 1) x
theorem LinearMap.hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasDerivAt (⇑e) (e 1) x
theorem LinearMap.hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasDerivWithinAt (⇑e) (e 1) s x
@[simp]
theorem LinearMap.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
deriv (⇑e) x = e 1
theorem LinearMap.derivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →ₗ[𝕜] F) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (⇑e) s x = e 1