The FrΓ©chet derivative #
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
has_fderiv_within_at f f' s x
says that f
has derivative f'
at x
, where the domain of interest
is restricted to s
. We also have
has_fderiv_at f f' x := has_fderiv_within_at f f' x univ
Finally,
has_strict_fderiv_at 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
is_bounded_bilinear_map.has_fderiv_at
twice: first for has_fderiv_at
, then for
has_strict_fderiv_at
.
Main results #
In addition to the definition and basic properties of the derivative, this file contains the usual formulas (and existence assertions) for the derivative of
- constants
- the identity
- bounded linear maps
- bounded bilinear maps
- sum of two functions
- sum of finitely many functions
- multiplication of a function by a scalar constant
- negative of a function
- subtraction of two functions
- multiplication of a function by a scalar function
- multiplication of two scalar functions
- composition of functions (the chain rule)
- inverse function (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 has_deriv_at
'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 β (Ξ» 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) : differentiable_at β (Ξ» 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 analysis.special_functions.trigonometric
.
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 #
The derivative is defined in terms of the is_o
relation, but also
characterized in terms of the tendsto
relation.
We also introduce predicates differentiable_within_at π 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 differentiable_at π f x
,
differentiable_on π f s
and differentiable π f
to express the existence of a derivative.
To be able to compute with derivatives, we write fderiv_within π 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 unique_diff_within_at s x
and
unique_diff_on s
, defined in tangent_cone.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.
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 (Ξ» 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
.
Tags #
derivative, differentiable, FrΓ©chet, calculus
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 has_fderiv_at
), giving rise to the usual notion
of FrΓ©chet derivative, and for L = π[s] x
(in has_fderiv_within_at
), giving rise to
the notion of FrΓ©chet derivative along the set s
.
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
- has_fderiv_within_at f f' s x = has_fderiv_at_filter f f' x (nhds_within x s)
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
- has_fderiv_at f f' x = has_fderiv_at_filter f f' x (nhds x)
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.
A function f
is differentiable at a point x
within a set s
if it admits a derivative
there (possibly non-unique).
Equations
- differentiable_within_at π f s x = β (f' : E βL[π] F), has_fderiv_within_at f f' s x
A function f
is differentiable at a point x
if it admits a derivative there (possibly
non-unique).
Equations
- differentiable_at π f x = β (f' : E βL[π] F), has_fderiv_at f f' x
If f
has a derivative at x
within s
, then fderiv_within π f s x
is such a derivative.
Otherwise, it is set to 0
.
Equations
- fderiv_within π f s x = dite (β (f' : E βL[π] F), has_fderiv_within_at f f' s x) (Ξ» (h : β (f' : E βL[π] F), has_fderiv_within_at f f' s x), classical.some h) (Ξ» (h : Β¬β (f' : E βL[π] F), has_fderiv_within_at f f' s x), 0)
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 = dite (β (f' : E βL[π] F), has_fderiv_at f f' x) (Ξ» (h : β (f' : E βL[π] F), has_fderiv_at f f' x), classical.some h) (Ξ» (h : Β¬β (f' : E βL[π] F), has_fderiv_at f f' x), 0)
differentiable_on π f s
means that f
is differentiable within s
at any point of s
.
Equations
- differentiable_on π f s = β (x : E), x β s β differentiable_within_at π f s x
differentiable π f
means that f
is differentiable at any point.
Equations
- differentiable π f = β (x : E), differentiable_at π f x
If a function f has a derivative f' at x, a rescaled version of f around x converges to f',
i.e., n (f (x + (1/n) v) - f x)
converges to f' v
. More generally, if c n
tends to infinity
and c n * d n
tends to v
, then c n * (f (x + d n) - f x)
tends to f' v
. This lemma expresses
this fact, for functions having a derivative within a set. Its specific formulation is useful for
tangent cone related discussions.
If f'
and fβ'
are two derivatives of f
within s
at x
, then they are equal on the
tangent cone to s
at x
unique_diff_within_at
achieves its goal: it implies the uniqueness of the derivative.
Basic properties of the derivative #
Converse to the mean value inequality: if f
is differentiable at xβ
and C
-lipschitz
on a neighborhood of xβ
then it its derivative at xβ
has norm bounded by C
. This version
only assumes that β₯f x - f xββ₯ β€ C * β₯x - xββ₯
in a neighborhood of x
.
Converse to the mean value inequality: if f
is differentiable at xβ
and C
-lipschitz
on a neighborhood of xβ
then it its derivative at xβ
has norm bounded by C
.
If f
is strictly differentiable at x
with derivative f'
and K > β₯f'β₯β
, then f
is
K
-Lipschitz in a neighborhood of x
.
If f
is strictly differentiable at x
with derivative f'
, then f
is Lipschitz in a
neighborhood of x
. See also has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt
for a
more precise statement.
Directional derivative agrees with has_fderiv
.
Converse to the mean value inequality: if f
is differentiable at xβ
and C
-lipschitz
on a neighborhood of xβ
then it its derivative at xβ
has norm bounded by C
.
Version using fderiv
.
If x
is not in the closure of s
, then f
has any derivative at x
within s
,
as this statement is empty.
Deducing continuity from differentiability #
congr properties of the derivative #
Derivative of the identity #
derivative of a constant function #
Continuous linear maps #
There are currently two variants of these in mathlib, the bundled version
(named continuous_linear_map
, and denoted E βL[π] F
), and the unbundled version (with a
predicate is_bounded_linear_map
). We give statements for both versions.
Derivative of the composition of two functions #
For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to get confused since there are too many possibilities for composition
The chain rule.
Ternary version of fderiv_within.comp
, with equality assumptions of basepoints added, in
order to apply more easily as a rewrite from right-to-left.
The chain rule for derivatives in the sense of strict differentiability.