# 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} :
HasStrictFDerivAt (βe) e x
theorem ContinuousLinearMap.hasFDerivAtFilter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} {L : } :
HasFDerivAtFilter (βe) e x L
theorem ContinuousLinearMap.hasFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} {s : Set E} :
HasFDerivWithinAt (βe) e s x
theorem ContinuousLinearMap.hasFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} :
HasFDerivAt (βe) e x
@[simp]
theorem ContinuousLinearMap.differentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} :
DifferentiableAt π (βe) x
theorem ContinuousLinearMap.differentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} {s : Set E} :
DifferentiableWithinAt π (βe) s x
@[simp]
theorem ContinuousLinearMap.fderiv {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {x : E} :
fderiv π (βe) x = e
theorem ContinuousLinearMap.fderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) :
Differentiable π βe
theorem ContinuousLinearMap.differentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (e : E βL[π] F) {s : Set E} :
DifferentiableOn π (βe) s
theorem IsBoundedLinearMap.hasFDerivAtFilter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {L : } (h : IsBoundedLinearMap π f) :
HasFDerivAtFilter f h.toContinuousLinearMap x L
theorem IsBoundedLinearMap.hasFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (h : IsBoundedLinearMap π f) :
HasFDerivWithinAt f h.toContinuousLinearMap s x
theorem IsBoundedLinearMap.hasFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (h : IsBoundedLinearMap π f) :
HasFDerivAt f h.toContinuousLinearMap x
theorem IsBoundedLinearMap.differentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (h : IsBoundedLinearMap π f) :
DifferentiableAt π f x
theorem IsBoundedLinearMap.differentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (h : IsBoundedLinearMap π f) :
DifferentiableWithinAt π f s x
theorem IsBoundedLinearMap.fderiv {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (h : IsBoundedLinearMap π f) :
fderiv π f x = h.toContinuousLinearMap
theorem IsBoundedLinearMap.fderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (h : IsBoundedLinearMap π f) (hxs : UniqueDiffWithinAt π s x) :
fderivWithin π f s x = h.toContinuousLinearMap
theorem IsBoundedLinearMap.differentiable {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (h : IsBoundedLinearMap π f) :
Differentiable π f
theorem IsBoundedLinearMap.differentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (h : IsBoundedLinearMap π f) :
DifferentiableOn π f s