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 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.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.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) {x : E} {L : Filter E} :

HasFDerivAtFilter (⇑f) f x L

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

HasFDerivAtFilter f (toContinuousLinearMap f 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 (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