The derivative of bounded linear maps

For detailed documentation of the Fréchet derivative, see the module docstring of Mathlib/Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of bounded linear maps.

Bundled continuous linear maps

There are currently two variants of these in mathlib, the bundled version (named ContinuousLinearMap, and denoted E →L[𝕜] F, works for topological vector spaces), and the unbundled version (with a predicate IsBoundedLinearMap, requires normed spaces). This section deals with the first form, see below for the unbundled version

theorem ContinuousLinearMap.hasFDerivAtFilter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {L : Filter (E × E)} : HasFDerivAtFilter (⇑f) f L

theorem ContinuousLinearMap.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} : HasStrictFDerivAt (⇑f) f x

theorem ContinuousLinearMap.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} {s : Set E} : HasFDerivWithinAt (⇑f) f s x

theorem ContinuousLinearMap.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} : HasFDerivAt (⇑f) f x

@[simp]

theorem ContinuousLinearMap.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} : DifferentiableAt 𝕜 (⇑f) x

theorem ContinuousLinearMap.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} {s : Set E} : DifferentiableWithinAt 𝕜 (⇑f) s x

@[simp]

theorem ContinuousLinearMap.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) : Differentiable 𝕜 ⇑f

theorem ContinuousLinearMap.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {s : Set E} : DifferentiableOn 𝕜 (⇑f) s

@[simp]

theorem ContinuousLinearMap.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F] : fderiv 𝕜 (⇑f) x = f

theorem ContinuousLinearMap.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F] (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (⇑f) s x = f

Unbundled continuous linear maps

theorem IsBoundedLinearMap.hasFDerivAtFilter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {L : Filter (E × E)} (h : IsBoundedLinearMap 𝕜 f) : HasFDerivAtFilter f (toContinuousLinearMap f h) L

theorem IsBoundedLinearMap.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : IsBoundedLinearMap 𝕜 f) : HasFDerivWithinAt f (toContinuousLinearMap f h) s x

theorem IsBoundedLinearMap.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : IsBoundedLinearMap 𝕜 f) : HasFDerivAt f (toContinuousLinearMap f h) x

theorem IsBoundedLinearMap.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : IsBoundedLinearMap 𝕜 f) : DifferentiableAt 𝕜 f x

theorem IsBoundedLinearMap.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : IsBoundedLinearMap 𝕜 f) : DifferentiableWithinAt 𝕜 f s x

theorem IsBoundedLinearMap.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : IsBoundedLinearMap 𝕜 f) : fderiv 𝕜 f x = toContinuousLinearMap f h

theorem IsBoundedLinearMap.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : IsBoundedLinearMap 𝕜 f) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 f s x = toContinuousLinearMap f h

theorem IsBoundedLinearMap.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (h : IsBoundedLinearMap 𝕜 f) : Differentiable 𝕜 f

theorem IsBoundedLinearMap.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : IsBoundedLinearMap 𝕜 f) : DifferentiableOn 𝕜 f s