Documentation

Mathlib.Analysis.Calculus.FDeriv.Linear

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 h.toContinuousLinearMap 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 h.toContinuousLinearMap 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 h.toContinuousLinearMap 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 = h.toContinuousLinearMap
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 = h.toContinuousLinearMap
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