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)
:
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)
:
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