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] {L : Filter (𝕜 × 𝕜)} (e : 𝕜 →L[𝕜] F) : HasDerivAtFilter (⇑e) (e 1) 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] {L : Filter (𝕜 × 𝕜)} (e : 𝕜 →ₗ[𝕜] F) : HasDerivAtFilter (⇑e) (e 1) 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