The Fréchet derivative: basic properties #

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.

Main results #

This file builds on the bare-bones definition given in Defs.lean by establishing a variety of relatively straightforward properties of the derivative.

Deeper properties are defined in other files in the folder Analysis/Calculus/FDeriv/, which contain the usual formulas (and existence assertions) for the derivative of

constants (Const.lean)
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)

For most binary operations we also define const_op and op_const theorems for the cases when the first or second argument is a constant. This makes writing chains of HasDerivAt's easier, and they more frequently lead to the desired result.

One can also interpret the derivative of a function f : 𝕜 → E as an element of E (by identifying a linear function from 𝕜 to E with its value at 1). Results on the Fréchet derivative are translated to this more elementary point of view on the derivative in the file Deriv.lean. The derivative of polynomials is handled there, as it is naturally one-dimensional.

The simplifier is set up to prove automatically that some functions are differentiable, or differentiable at a point (but not differentiable on a set or within a set at a point, as checking automatically that the good domains are mapped one to the other when using composition is not something the simplifier can easily do). This means that one can write example (x : ℝ) : Differentiable ℝ (fun x ↦ sin (exp (3 + x^2)) - 5 * cos x) := by simp. If there are divisions, one needs to supply to the simplifier proofs that the denominators do not vanish, as in

example (x : ℝ) (h : 1 + sin x ≠ 0) : DifferentiableAt ℝ (fun x ↦ exp x / (1 + sin x)) x := by
  simp [h]

Of course, these examples only work once exp, cos and sin have been shown to be differentiable, in Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean.

The simplifier is not set up to compute the Fréchet derivative of maps (as these are in general complicated multidimensional linear maps), but it will compute one-dimensional derivatives, see Deriv.lean.

Implementation details #

For a discussion of the definitions and their rationale, see the file docstring of Mathlib.Analysis.Calculus.FDeriv.Defs.

To make sure that the simplifier can prove automatically that functions are differentiable, we tag many lemmas with the simp attribute, for instance those saying that the sum of differentiable functions is differentiable, as well as their product, their cartesian product, and so on. A notable exception is the chain rule: we do not mark as a simp lemma the fact that, if f and g are differentiable, then their composition also is: simp would always be able to match this lemma, by taking f or g to be the identity. Instead, for every reasonable function (say, exp), we add a lemma that if f is differentiable then so is (fun x ↦ exp (f x)). This means adding some boilerplate lemmas, but these can also be useful in their own right.

Tests for this ability of the simplifier (with more examples) are provided in Tests/Differentiable.lean.

TODO #

Generalize more results to topological vector spaces.

Tags #

derivative, differentiable, Fréchet, calculus

The Fréchet derivative: basic properties #

Main results #

Implementation details #

TODO #

Tags #

Basic properties of the derivative #

Deducing continuity from differentiability #

Derivative of the identity #

Results involving semilinear maps #