The Fréchet derivative: definition

Let E and F be normed spaces, f : E → F, and f' : E →L[𝕜] F a continuous 𝕜-linear map, where 𝕜 is a non-discrete normed field. Then

HasFDerivWithinAt f f' s x

says that f has derivative f' at x, where the domain of interest is restricted to s. We also have

HasFDerivAt f f' x := HasFDerivWithinAt f f' x univ

Finally,

HasStrictFDerivAt f f' x

means that f : E → F has derivative f' : E →L[𝕜] F in the sense of strict differentiability, i.e., f y - f z - f'(y - z) = o(y - z) as y, z → x. This notion is used in the inverse function theorem, and is defined here only to avoid proving theorems like IsBoundedBilinearMap.hasFDerivAt twice: first for HasFDerivAt, then for HasStrictFDerivAt.

This file Defs.lean is intended to just contain the definitions and the bare minimum of supporting lemmas; a much wider range of elementary properties are proved in the file Basic.lean.

Other files in the folder Analysis/Calculus/FDeriv/ contain the usual formulas (and existence assertions) for the derivative of

• constants (Const.lean)
• the identity
• bounded linear maps (Linear.lean)
• bounded bilinear maps (Bilinear.lean)
• sum of two functions (Add.lean)
• sum of finitely many functions (Add.lean)
• multiplication of a function by a scalar constant (Add.lean)
• negative of a function (Add.lean)
• subtraction of two functions (Add.lean)
• multiplication of a function by a scalar function (Mul.lean)
• multiplication of two scalar functions (Mul.lean)
• composition of functions (the chain rule) (Comp.lean)
• inverse function (Mul.lean) (assuming that it exists; the inverse function theorem is in ../Inverse.lean)

Implementation details

The derivative is defined in terms of the IsLittleOTVS relation to ensure the definition does not ingrain a choice of norm, and is then quickly translated to the more convenient IsLittleO in the subsequent theorems. It is also characterized in terms of the Tendsto relation.

We also introduce predicates DifferentiableWithinAt 𝕜 f s x (where 𝕜 is the base field, f the function to be differentiated, x the point at which the derivative is asserted to exist, and s the set along which the derivative is defined), as well as DifferentiableAt 𝕜 f x, DifferentiableOn 𝕜 f s and Differentiable 𝕜 f to express the existence of a derivative.

To be able to compute with derivatives, we write fderivWithin 𝕜 f s x and fderiv 𝕜 f x for some choice of a derivative if it exists, and the zero function otherwise. This choice only behaves well along sets for which the derivative is unique, i.e., those for which the tangent directions span a dense subset of the whole space. The predicates UniqueDiffWithinAt s x and UniqueDiffOn s, defined in TangentCone.lean express this property. We prove that indeed they imply the uniqueness of the derivative. This is satisfied for open subsets, and in particular for univ. This uniqueness only holds when the field is non-discrete, which we request at the very beginning: otherwise, a derivative can be defined, but it has no interesting properties whatsoever.

TODO

Generalize more results to topological vector spaces.

Tags

derivative, differentiable, Fréchet, calculus

Definitions valid in an arbitrary topological vector space

structure 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 → F) (f' : E →L[𝕜] F) (x : E) (L : Filter E) : Prop

A function f has the continuous linear map f' as derivative along the filter L if f x' = f x + f' (x' - x) + o (x' - x) when x' converges along the filter L. This definition is designed to be specialized for L = 𝓝 x (in HasFDerivAt), giving rise to the usual notion of Fréchet derivative, and for L = 𝓝[s] x (in HasFDerivWithinAt), giving rise to the notion of Fréchet derivative along the set s.

• of_isLittleOTVS :: (
• isLittleOTVS : (fun (x' : E) => f x' - f x - f' (x' - x)) =o[𝕜; L] fun (x' : E) => x' - x
• )

theorem hasFDerivAtFilter_iff_isLittleOTVS {𝕜 : 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 → F) (f' : E →L[𝕜] F) (x : E) (L : Filter E) : HasFDerivAtFilter f f' x L ↔ (fun (x' : E) => f x' - f x - f' (x' - x)) =o[𝕜; L] fun (x' : E) => x' - x

def 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 → F) (f' : E →L[𝕜] F) (s : Set E) (x : E) : Prop

A function f has the continuous linear map f' as derivative at x within a set s if f x' = f x + f' (x' - x) + o (x' - x) when x' tends to x inside s.

Equations

• HasFDerivWithinAt f f' s x = HasFDerivAtFilter f f' x (nhdsWithin x s)

def 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 → F) (f' : E →L[𝕜] F) (x : E) : Prop

A function f has the continuous linear map f' as derivative at x if f x' = f x + f' (x' - x) + o (x' - x) when x' tends to x.

Equations

• HasFDerivAt f f' x = HasFDerivAtFilter f f' x (nhds x)

structure 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 → F) (f' : E →L[𝕜] F) (x : E) : Prop

A function f has derivative f' at a in the sense of strict differentiability if f x - f y - f' (x - y) = o(x - y) as x, y → a. This form of differentiability is required, e.g., by the inverse function theorem. Any C^1 function on a vector space over ℝ is strictly differentiable but this definition works, e.g., for vector spaces over p-adic numbers.

• of_isLittleOTVS :: (
• isLittleOTVS : (fun (p : E × E) => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; nhds (x, x)] fun (p : E × E) => p.1 - p.2
• )

theorem hasStrictFDerivAt_iff_isLittleOTVS {𝕜 : 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 → F) (f' : E →L[𝕜] F) (x : E) : HasStrictFDerivAt f f' x ↔ (fun (p : E × E) => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; nhds (x, x)] fun (p : E × E) => p.1 - p.2

def 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 → F) (s : Set E) (x : E) : Prop

A function f is differentiable at a point x within a set s if it admits a derivative there (possibly non-unique).

Equations

• DifferentiableWithinAt 𝕜 f s x = ∃ (f' : E →L[𝕜] F), HasFDerivWithinAt f f' s x

def 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 → F) (x : E) : Prop

A function f is differentiable at a point x if it admits a derivative there (possibly non-unique).

Equations

• DifferentiableAt 𝕜 f x = ∃ (f' : E →L[𝕜] F), HasFDerivAt f f' x

@[irreducible]

def fderivWithin (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : E →L[𝕜] F

If f has a derivative at x within s, then fderivWithin 𝕜 f s x is such a derivative. Otherwise, it is set to 0. We also set it to be zero, if zero is one of possible derivatives.

Equations

• fderivWithin 𝕜 f s x = if HasFDerivWithinAt f 0 s x then 0 else if h : DifferentiableWithinAt 𝕜 f s x then Classical.choose h else 0

theorem fderivWithin_def (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : fderivWithin 𝕜 f s x = if HasFDerivWithinAt f 0 s x then 0 else if h : DifferentiableWithinAt 𝕜 f s x then Classical.choose h else 0

@[irreducible]

def fderiv (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (x : E) : E →L[𝕜] F

If f has a derivative at x, then fderiv 𝕜 f x is such a derivative. Otherwise, it is set to 0.

Equations

• fderiv 𝕜 f x = fderivWithin 𝕜 f Set.univ x

theorem fderiv_def (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (x : E) : fderiv 𝕜 f x = fderivWithin 𝕜 f Set.univ x

def 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 → F) (s : Set E) : Prop

DifferentiableOn 𝕜 f s means that f is differentiable within s at any point of s.

Equations

• DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

def 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 → F) : Prop

Differentiable 𝕜 f means that f is differentiable at any point.

Equations

• Differentiable 𝕜 f = ∀ (x : E), DifferentiableAt 𝕜 f x

theorem fderivWithin_zero_of_not_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 → F} {x : E} {s : Set E} (h : ¬DifferentiableWithinAt 𝕜 f s x) : fderivWithin 𝕜 f s x = 0

@[simp]

theorem fderivWithin_univ {𝕜 : 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 → F} : fderivWithin 𝕜 f Set.univ = fderiv 𝕜 f

Reformulations for normed spaces

theorem hasFDerivAtFilter_iff_isLittleO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter E} : HasFDerivAtFilter f f' x L ↔ (fun (x' : E) => f x' - f x - f' (x' - x)) =o[L] fun (x' : E) => x' - x

theorem HasFDerivAtFilter.isLittleO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter E} : HasFDerivAtFilter f f' x L → (fun (x' : E) => f x' - f x - f' (x' - x)) =o[L] fun (x' : E) => x' - x

Alias of the forward direction of hasFDerivAtFilter_iff_isLittleO.

theorem HasFDerivAtFilter.of_isLittleO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter E} : ((fun (x' : E) => f x' - f x - f' (x' - x)) =o[L] fun (x' : E) => x' - x) → HasFDerivAtFilter f f' x L

Alias of the reverse direction of hasFDerivAtFilter_iff_isLittleO.

theorem hasStrictFDerivAt_iff_isLittleO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} : HasStrictFDerivAt f f' x ↔ (fun (p : E × E) => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun (p : E × E) => p.1 - p.2

theorem HasStrictFDerivAt.isLittleO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} : HasStrictFDerivAt f f' x → (fun (p : E × E) => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun (p : E × E) => p.1 - p.2

Alias of the forward direction of hasStrictFDerivAt_iff_isLittleO.

theorem HasStrictFDerivAt.of_isLittleO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} : ((fun (p : E × E) => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun (p : E × E) => p.1 - p.2) → HasStrictFDerivAt f f' x

Alias of the reverse direction of hasStrictFDerivAt_iff_isLittleO.