The derivative of bounded linear maps

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

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

Continuous linear maps

There are currently two variants of these in mathlib, the bundled version (named ContinuousLinearMap, and denoted E →L[𝕜] F), and the unbundled version (with a predicate IsBoundedLinearMap). We give statements for both versions.

theorem ContinuousLinearMap.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} : HasStrictFDerivAt (⇑e) e x

theorem ContinuousLinearMap.hasFDerivAtFilter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} {L : Filter E} : HasFDerivAtFilter (⇑e) e x L

theorem ContinuousLinearMap.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} {s : Set E} : HasFDerivWithinAt (⇑e) e s x

theorem ContinuousLinearMap.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} : HasFDerivAt (⇑e) e x

@[simp]

theorem ContinuousLinearMap.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} : DifferentiableAt 𝕜 (⇑e) x

theorem ContinuousLinearMap.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} {s : Set E} : DifferentiableWithinAt 𝕜 (⇑e) s x

@[simp]

theorem ContinuousLinearMap.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} : fderiv 𝕜 (⇑e) x = e

theorem ContinuousLinearMap.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} {s : Set E} (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (⇑e) s x = e

@[simp]

theorem ContinuousLinearMap.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) : Differentiable 𝕜 ⇑e

theorem ContinuousLinearMap.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →L[𝕜] F) {s : Set E} : DifferentiableOn 𝕜 (⇑e) s

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} {x : E} {L : Filter E} (h : IsBoundedLinearMap 𝕜 f) : HasFDerivAtFilter f (IsBoundedLinearMap.toContinuousLinearMap h) x 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 (IsBoundedLinearMap.toContinuousLinearMap 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 (IsBoundedLinearMap.toContinuousLinearMap 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 = IsBoundedLinearMap.toContinuousLinearMap 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 = IsBoundedLinearMap.toContinuousLinearMap 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