One-dimensional derivatives #
This file defines the derivative of a function f : π β F
where π
is a
normed field and F
is a normed space over this field. The derivative of
such a function f
at a point x
is given by an element f' : F
.
The theory is developed analogously to the FrΓ©chet derivatives. We first introduce predicates defined in terms of the corresponding predicates for FrΓ©chet derivatives:
-
has_deriv_at_filter f f' x L
states that the functionf
has the derivativef'
at the pointx
asx
goes along the filterL
. -
has_deriv_within_at f f' s x
states that the functionf
has the derivativef'
at the pointx
within the subsets
. -
has_deriv_at f f' x
states that the functionf
has the derivativef'
at the pointx
. -
has_strict_deriv_at f f' x
states that the functionf
has the derivativef'
at the pointx
in the sense of strict differentiability, i.e.,f y - f z = (y - z) β’ f' + o (y - z)
asy, z β x
.
For the last two notions we also define a functional version:
-
deriv_within f s x
is a derivative off
atx
withins
. If the derivative does not exist, thenderiv_within f s x
equals zero. -
deriv f x
is a derivative off
atx
. If the derivative does not exist, thenderiv f x
equals zero.
The theorems fderiv_within_deriv_within
and fderiv_deriv
show that the
one-dimensional derivatives coincide with the general FrΓ©chet derivatives.
We also show the existence and compute the derivatives of:
- constants
- the identity function
- linear maps
- addition
- sum of finitely many functions
- negation
- subtraction
- multiplication
- inverse
x β xβ»ΒΉ
- multiplication of two functions in
π β π
- multiplication of a function in
π β π
and of a function inπ β E
- composition of a function in
π β F
with a function inπ β π
- composition of a function in
F β E
with a function inπ β F
- inverse function (assuming that it exists; the inverse function theorem is in
inverse.lean
) - division
- polynomials
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.
We set up the simplifier so that it can compute the derivative of simple functions. For instance,
example (x : β) : deriv (Ξ» x, cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) :=
by { simp, ring }
Implementation notes #
Most of the theorems are direct restatements of the corresponding theorems for FrΓ©chet derivatives.
The strategy to construct simp lemmas that give the simplifier the possibility to compute
derivatives is the same as the one for differentiability statements, as explained in fderiv.lean
.
See the explanations there.
f
has the derivative f'
at the point x
as x
goes along the filter L
.
That is, f x' = f x + (x' - x) β’ f' + o(x' - x)
where x'
converges along the filter L
.
Equations
- has_deriv_at_filter f f' x L = has_fderiv_at_filter f (1.smul_right f') x L
f
has the derivative f'
at the point x
within the subset s
.
That is, f x' = f x + (x' - x) β’ f' + o(x' - x)
where x'
converges to x
inside s
.
Equations
- has_deriv_within_at f f' s x = has_deriv_at_filter f f' x (nhds_within x s)
f
has the derivative f'
at the point x
.
That is, f x' = f x + (x' - x) β’ f' + o(x' - x)
where x'
converges to x
.
Equations
- has_deriv_at f f' x = has_deriv_at_filter f f' x (nhds x)
f
has the derivative f'
at the point x
in the sense of strict differentiability.
That is, f y - f z = (y - z) β’ f' + o(y - z)
as y, z β x
.
Equations
- has_strict_deriv_at f f' x = has_strict_fderiv_at f (1.smul_right f') x
Derivative of f
at the point x
within the set s
, if it exists. Zero otherwise.
If the derivative exists (i.e., β f', has_deriv_within_at f f' s x
), then
f x' = f x + (x' - x) β’ deriv_within f s x + o(x' - x)
where x'
converges to x
inside s
.
Equations
- deriv_within f s x = β(fderiv_within π f s x) 1
Derivative of f
at the point x
, if it exists. Zero otherwise.
If the derivative exists (i.e., β f', has_deriv_at f f' x
), then
f x' = f x + (x' - x) β’ deriv f x + o(x' - x)
where x'
converges to x
.
Expressing has_fderiv_at_filter f f' x L
in terms of has_deriv_at_filter
Expressing has_fderiv_within_at f f' s x
in terms of has_deriv_within_at
Expressing has_deriv_within_at f f' s x
in terms of has_fderiv_within_at
Expressing has_fderiv_at f f' x
in terms of has_deriv_at
Alias of the forward direction of has_strict_deriv_at_iff_has_strict_fderiv_at
.
Expressing has_deriv_at f f' x
in terms of has_fderiv_at
Alias of the forward direction of has_deriv_at_iff_has_fderiv_at
.
If the domain has dimension one, then FrΓ©chet derivative is equivalent to the classical
definition with a limit. In this version we have to take the limit along the subset -{x}
,
because for y=x
the slope equals zero due to the convention 0β»ΒΉ=0
.
Alias of the forward direction of has_deriv_within_at_congr_set
.
Alias of the reverse direction of has_deriv_within_at_Ioi_iff_Ici
.
Alias of the forward direction of has_deriv_within_at_Ioi_iff_Ici
.
Alias of the forward direction of has_deriv_within_at_Iio_iff_Iic
.
Alias of the reverse direction of has_deriv_within_at_Iio_iff_Iic
.
Alias of the reverse direction of has_deriv_within_at.Ioi_iff_Ioo
.
Alias of the forward direction of has_deriv_within_at.Ioi_iff_Ioo
.
Congruence properties of derivatives #
Derivative of the identity #
Derivative of constant functions #
Derivative of continuous linear maps #
Derivative of bundled linear maps #
Derivative of the sum of two functions #
Derivative of a finite sum of functions #
Derivatives of functions f : π β Ξ i, E i
#
Derivative of the multiplication of a scalar function and a vector function #
Derivative of the negative of a function #
Derivative of the negation function (i.e has_neg.neg
) #
Derivative of the difference of two functions #
Continuity of a function admitting a derivative #
Derivative of the cartesian product of two functions #
Derivative of the composition of a vector function and a scalar function #
We use scomp
in lemmas on composition of vector valued and scalar valued functions, and comp
in lemmas on composition of scalar valued functions, in analogy for smul
and mul
(and also
because the comp
version with the shorter name will show up much more often in applications).
The formula for the derivative involves smul
in scomp
lemmas, which can be reduced to
usual multiplication in comp
lemmas.
The chain rule.
Derivative of the composition of a scalar and vector functions #
Derivative of the composition of two scalar functions #
The chain rule.
Derivative of the composition of a function between vector spaces and a function on π
#
The composition l β f
where l : F β E
and f : π β F
, has a derivative within a set
equal to the FrΓ©chet derivative of l
applied to the derivative of f
.
The composition l β f
where l : F β E
and f : π β F
, has a derivative equal to the
FrΓ©chet derivative of l
applied to the derivative of f
.
Derivative of the multiplication of two functions #
Derivative of x β¦ xβ»ΒΉ
#
Derivative of x β¦ c x / d x
#
Derivative of the pointwise composition/application of continuous linear maps #
If f (g y) = y
for y
in some neighborhood of a
, g
is continuous at a
, and f
has an
invertible derivative f'
at g a
in the strict sense, then g
has the derivative f'β»ΒΉ
at a
in the strict sense.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.