Higher differentiability #
A function is C^1
on a domain if it is differentiable there, and its derivative is continuous.
By induction, it is C^n
if it is C^{n-1}
and its (n-1)-th derivative is C^1
there or,
equivalently, if it is C^1
and its derivative is C^{n-1}
.
Finally, it is C^β
if it is C^n
for all n.
We formalize these notions by defining iteratively the n+1
-th derivative of a function as the
derivative of the n
-th derivative. It is called iterated_fderiv π n f x
where π
is the
field, n
is the number of iterations, f
is the function and x
is the point, and it is given
as an n
-multilinear map. We also define a version iterated_fderiv_within
relative to a domain,
as well as predicates times_cont_diff_within_at
, times_cont_diff_at
, times_cont_diff_on
and
times_cont_diff
saying that the function is C^n
within a set at a point, at a point, on a set
and on the whole space respectively.
To avoid the issue of choice when choosing a derivative in sets where the derivative is not
necessarily unique, times_cont_diff_on
is not defined directly in terms of the
regularity of the specific choice iterated_fderiv_within π n f s
inside s
, but in terms of the
existence of a nice sequence of derivatives, expressed with a predicate
has_ftaylor_series_up_to_on
.
We prove basic properties of these notions.
Main definitions and results #
Let f : E β F
be a map between normed vector spaces over a nondiscrete normed field π
.
has_ftaylor_series_up_to n f p
: expresses that the formal multilinear seriesp
is a sequence of iterated derivatives off
, up to then
-th term (wheren
is a natural number orβ
).has_ftaylor_series_up_to_on n f p s
: same thing, but inside a sets
. The notion of derivative is now taken insides
. In particular, derivatives don't have to be unique.times_cont_diff π n f
: expresses thatf
isC^n
, i.e., it admits a Taylor series up to rankn
.times_cont_diff_on π n f s
: expresses thatf
isC^n
ins
.times_cont_diff_at π n f x
: expresses thatf
isC^n
aroundx
.times_cont_diff_within_at π n f s x
: expresses thatf
isC^n
aroundx
within the sets
.iterated_fderiv_within π n f s x
is ann
-th derivative off
over the fieldπ
on the sets
at the pointx
. It is a continuous multilinear map fromE^n
toF
, defined as a derivative withins
ofiterated_fderiv_within π (n-1) f s
if one exists, and0
otherwise.iterated_fderiv π n f x
is then
-th derivative off
over the fieldπ
at the pointx
. It is a continuous multilinear map fromE^n
toF
, defined as a derivative ofiterated_fderiv π (n-1) f
if one exists, and0
otherwise.
In sets of unique differentiability, times_cont_diff_on π n f s
can be expressed in terms of the
properties of iterated_fderiv_within π m f s
for m β€ n
. In the whole space,
times_cont_diff π n f
can be expressed in terms of the properties of iterated_fderiv π m f
for m β€ n
.
We also prove that the usual operations (addition, multiplication, difference, composition, and
so on) preserve C^n
functions.
Implementation notes #
The definitions in this file are designed to work on any field π
. They are sometimes slightly more
complicated than the naive definitions one would guess from the intuition over the real or complex
numbers, but they are designed to circumvent the lack of gluing properties and partitions of unity
in general. In the usual situations, they coincide with the usual definitions.
Definition of C^n
functions in domains #
One could define C^n
functions in a domain s
by fixing an arbitrary choice of derivatives (this
is what we do with iterated_fderiv_within
) and requiring that all these derivatives up to n
are
continuous. If the derivative is not unique, this could lead to strange behavior like two C^n
functions f
and g
on s
whose sum is not C^n
. A better definition is thus to say that a
function is C^n
inside s
if it admits a sequence of derivatives up to n
inside s
.
This definition still has the problem that a function which is locally C^n
would not need to
be C^n
, as different choices of sequences of derivatives around different points might possibly
not be glued together to give a globally defined sequence of derivatives. (Note that this issue
can not happen over reals, thanks to partition of unity, but the behavior over a general field is
not so clear, and we want a definition for general fields). Also, there are locality
problems for the order parameter: one could image a function which, for each n
, has a nice
sequence of derivatives up to order n
, but they do not coincide for varying n
and can therefore
not be glued to give rise to an infinite sequence of derivatives. This would give a function
which is C^n
for all n
, but not C^β
. We solve this issue by putting locality conditions
in space and order in our definition of times_cont_diff_within_at
and times_cont_diff_on
.
The resulting definition is slightly more complicated to work with (in fact not so much), but it
gives rise to completely satisfactory theorems.
For instance, with this definition, a real function which is C^m
(but not better) on (-1/m, 1/m)
for each natural m
is by definition C^β
at 0
.
There is another issue with the definition of times_cont_diff_within_at π n f s x
. We can
require the existence and good behavior of derivatives up to order n
on a neighborhood of x
within s
. However, this does not imply continuity or differentiability within s
of the function
at x
when x
does not belong to s
. Therefore, we require such existence and good behavior on
a neighborhood of x
within s βͺ {x}
(which appears as insert x s
in this file).
Side of the composition, and universe issues #
With a naΓ―ve direct definition, the n
-th derivative of a function belongs to the space
E βL[π] (E βL[π] (E ... F)...)))
where there are n iterations of E βL[π]
. This space
may also be seen as the space of continuous multilinear functions on n
copies of E
with
values in F
, by uncurrying. This is the point of view that is usually adopted in textbooks,
and that we also use. This means that the definition and the first proofs are slightly involved,
as one has to keep track of the uncurrying operation. The uncurrying can be done from the
left or from the right, amounting to defining the n+1
-th derivative either as the derivative of
the n
-th derivative, or as the n
-th derivative of the derivative.
For proofs, it would be more convenient to use the latter approach (from the right),
as it means to prove things at the n+1
-th step we only need to understand well enough the
derivative in E βL[π] F
(contrary to the approach from the left, where one would need to know
enough on the n
-th derivative to deduce things on the n+1
-th derivative).
However, the definition from the right leads to a universe polymorphism problem: if we define
iterated_fderiv π (n + 1) f x = iterated_fderiv π n (fderiv π f) x
by induction, we need to
generalize over all spaces (as f
and fderiv π f
don't take values in the same space). It is
only possible to generalize over all spaces in some fixed universe in an inductive definition.
For f : E β F
, then fderiv π f
is a map E β (E βL[π] F)
. Therefore, the definition will only
work if F
and E βL[π] F
are in the same universe.
This issue does not appear with the definition from the left, where one does not need to generalize
over all spaces. Therefore, we use the definition from the left. This means some proofs later on
become a little bit more complicated: to prove that a function is C^n
, the most efficient approach
is to exhibit a formula for its n
-th derivative and prove it is continuous (contrary to the
inductive approach where one would prove smoothness statements without giving a formula for the
derivative). In the end, this approach is still satisfactory as it is good to have formulas for the
iterated derivatives in various constructions.
One point where we depart from this explicit approach is in the proof of smoothness of a
composition: there is a formula for the n
-th derivative of a composition (FaΓ di Bruno's formula),
but it is very complicated and barely usable, while the inductive proof is very simple. Thus, we
give the inductive proof. As explained above, it works by generalizing over the target space, hence
it only works well if all spaces belong to the same universe. To get the general version, we lift
things to a common universe using a trick.
Variables management #
The textbook definitions and proofs use various identifications and abuse of notations, for instance
when saying that the natural space in which the derivative lives, i.e.,
E βL[π] (E βL[π] ( ... βL[π] F))
, is the same as a space of multilinear maps. When doing things
formally, we need to provide explicit maps for these identifications, and chase some diagrams to see
everything is compatible with the identifications. In particular, one needs to check that taking the
derivative and then doing the identification, or first doing the identification and then taking the
derivative, gives the same result. The key point for this is that taking the derivative commutes
with continuous linear equivalences. Therefore, we need to implement all our identifications with
continuous linear equivs.
Notations #
We use the notation E [Γn]βL[π] F
for the space of continuous multilinear maps on E^n
with
values in F
. This is the space in which the n
-th derivative of a function from E
to F
lives.
In this file, we denote β€ : with_top β
with β
.
Tags #
derivative, differentiability, higher derivative, C^n
, multilinear, Taylor series, formal series
Functions with a Taylor series on a domain #
- zero_eq : β (x : E), x β s β (p x 0).uncurry0 = f x
- fderiv_within : β (m : β), βm < n β β (x : E), x β s β has_fderiv_within_at (Ξ» (y : E), p y m) (p x m.succ).curry_left s x
- cont : β (m : β), βm β€ n β continuous_on (Ξ» (x : E), p x m) s
has_ftaylor_series_up_to_on n f p s
registers the fact that p 0 = f
and p (m+1)
is a
derivative of p m
for m < n
, and is continuous for m β€ n
. This is a predicate analogous to
has_fderiv_within_at
but for higher order derivatives.
If two functions coincide on a set s
, then a Taylor series for the first one is as well a
Taylor series for the second one.
If a function has a Taylor series at order at least 1
, then the term of order 1
of this
series is a derivative of f
.
If a function has a Taylor series at order at least 1
on a neighborhood of x
, then the term
of order 1
of this series is a derivative of f
at x
.
If a function has a Taylor series at order at least 1
on a neighborhood of x
, then
in a neighborhood of x
, the term of order 1
of this series is a derivative of f
.
If a function has a Taylor series at order at least 1
on a neighborhood of x
, then
it is differentiable at x
.
p
is a Taylor series of f
up to n+1
if and only if p
is a Taylor series up to n
, and
p (n + 1)
is a derivative of p n
.
p
is a Taylor series of f
up to n+1
if and only if p.shift
is a Taylor series up to n
for p 1
, which is a derivative of f
.
Smooth functions within a set around a point #
A function is continuously differentiable up to order n
within a set s
at a point x
if
it admits continuous derivatives up to order n
in a neighborhood of x
in s βͺ {x}
.
For n = β
, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
For instance, a real function which is C^m
on (-1/m, 1/m)
for each natural m
, but not
better, is C^β
at 0
within univ
.
Equations
- times_cont_diff_within_at π n f s x = β (m : β), βm β€ n β (β (u : set E) (H : u β π[insert x s] x) (p : E β formal_multilinear_series π E F), has_ftaylor_series_up_to_on βm f p u)
If a function is C^n
within a set at a point, with n β₯ 1
, then it is differentiable
within this set at this point.
A function is C^(n + 1)
on a domain iff locally, it has a derivative which is C^n
.
Smooth functions within a set #
A function is continuously differentiable up to n
on s
if, for any point x
in s
, it
admits continuous derivatives up to order n
on a neighborhood of x
in s
.
For n = β
, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
Equations
- times_cont_diff_on π n f s = β (x : E), x β s β times_cont_diff_within_at π n f s x
If a function is C^n
on a set with n β₯ 1
, then it is differentiable there.
If a function is C^n
around each point in a set, then it is C^n
on the set.
A function is C^(n + 1)
on a domain iff locally, it has a derivative which is C^n
.
Iterated derivative within a set #
The n
-th derivative of a function along a set, defined inductively by saying that the n+1
-th
derivative of f
is the derivative of the n
-th derivative of f
along this set, together with
an uncurrying step to see it as a multilinear map in n+1
variables..
Equations
- iterated_fderiv_within π n f s = n.rec_on (Ξ» (x : E), continuous_multilinear_map.curry0 π E (f x)) (Ξ» (n : β) (rec : E β continuous_multilinear_map π (Ξ» (i : fin n), E) F) (x : E), (fderiv_within π rec s x).uncurry_left)
Formal Taylor series associated to a function within a set.
Equations
- ftaylor_series_within π f s x = Ξ» (n : β), iterated_fderiv_within π n f s x
Writing explicitly the n+1
-th derivative as the composition of a currying linear equiv,
and the derivative of the n
-th derivative.
Writing explicitly the n+1
-th derivative as the composition of a currying linear equiv,
and the n
-th derivative of the derivative.
If two functions coincide on a set s
of unique differentiability, then their iterated
differentials within this set coincide.
The iterated differential within a set s
at a point x
is not modified if one intersects
s
with an open set containing x
.
The iterated differential within a set s
at a point x
is not modified if one intersects
s
with a neighborhood of x
within s
.
The iterated differential within a set s
at a point x
is not modified if one intersects
s
with a neighborhood of x
.
On a set with unique differentiability, any choice of iterated differential has to coincide
with the one we have chosen in iterated_fderiv_within π m f s
.
When a function is C^n
in a set s
of unique differentiability, it admits
ftaylor_series_within π f s
as a Taylor series up to order n
in s
.
A function is C^(n + 1)
on a domain with unique derivatives if and only if it is
differentiable there, and its derivative (expressed with fderiv_within
) is C^n
.
A function is C^(n + 1)
on an open domain if and only if it is
differentiable there, and its derivative (expressed with fderiv
) is C^n
.
A function is C^β
on a domain with unique derivatives if and only if it is differentiable
there, and its derivative (expressed with fderiv_within
) is C^β
.
A function is C^β
on an open domain if and only if it is differentiable there, and its
derivative (expressed with fderiv
) is C^β
.
If a function is at least C^1
, its bundled derivative (mapping (x, v)
to Df(x) v
) is
continuous.
Functions with a Taylor series on the whole space #
- zero_eq : β (x : E), (p x 0).uncurry0 = f x
- fderiv : β (m : β), βm < n β β (x : E), has_fderiv_at (Ξ» (y : E), p y m) (p x m.succ).curry_left x
- cont : β (m : β), βm β€ n β continuous (Ξ» (x : E), p x m)
has_ftaylor_series_up_to n f p
registers the fact that p 0 = f
and p (m+1)
is a
derivative of p m
for m < n
, and is continuous for m β€ n
. This is a predicate analogous to
has_fderiv_at
but for higher order derivatives.
If a function has a Taylor series at order at least 1
, then the term of order 1
of this
series is a derivative of f
.
p
is a Taylor series of f
up to n+1
if and only if p.shift
is a Taylor series up to n
for p 1
, which is a derivative of f
.
Smooth functions at a point #
A function is continuously differentiable up to n
at a point x
if, for any integer k β€ n
,
there is a neighborhood of x
where f
admits derivatives up to order n
, which are continuous.
Equations
- times_cont_diff_at π n f x = times_cont_diff_within_at π n f set.univ x
If a function is C^n
with n β₯ 1
at a point, then it is differentiable there.
A function is C^(n + 1)
at a point iff locally, it has a derivative which is C^n
.
Smooth functions #
A function is continuously differentiable up to n
if it admits derivatives up to
order n
, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
Equations
- times_cont_diff π n f = β (p : E β formal_multilinear_series π E F), has_ftaylor_series_up_to n f p
If a function is C^n
with n β₯ 1
, then it is differentiable.
Iterated derivative #
The n
-th derivative of a function, as a multilinear map, defined inductively.
Equations
- iterated_fderiv π n f = n.rec_on (Ξ» (x : E), continuous_multilinear_map.curry0 π E (f x)) (Ξ» (n : β) (rec : E β continuous_multilinear_map π (Ξ» (i : fin n), E) F) (x : E), (fderiv π rec x).uncurry_left)
Formal Taylor series associated to a function within a set.
Equations
- ftaylor_series π f x = Ξ» (n : β), iterated_fderiv π n f x
Writing explicitly the n+1
-th derivative as the composition of a currying linear equiv,
and the derivative of the n
-th derivative.
Writing explicitly the n+1
-th derivative as the composition of a currying linear equiv,
and the n
-th derivative of the derivative.
When a function is C^n
in a set s
of unique differentiability, it admits
ftaylor_series_within π f s
as a Taylor series up to order n
in s
.
A function is C^(n + 1)
on a domain with unique derivatives if and only if
it is differentiable there, and its derivative is C^n
.
A function is C^β
on a domain with unique derivatives if and only if it is differentiable
there, and its derivative is C^β
.
If a function is at least C^1
, its bundled derivative (mapping (x, v)
to Df(x) v
) is
continuous.
Constants #
Constants are C^β
.
Linear functions #
Unbundled bounded linear functions are C^β
.
The first projection in a product is C^β
.
The first projection on a domain in a product is C^β
.
The first projection at a point in a product is C^β
.
The first projection within a domain at a point in a product is C^β
.
The second projection in a product is C^β
.
The second projection on a domain in a product is C^β
.
The second projection at a point in a product is C^β
.
The second projection within a domain at a point in a product is C^β
.
The identity is C^β
.
Bilinear functions are C^β
.
If f
admits a Taylor series p
in a set s
, and g
is linear, then g β f
admits a Taylor
series whose k
-th term is given by g β (p k)
.
Composition by continuous linear maps on the left preserves C^n
functions in a domain
at a point.
Composition by continuous linear maps on the left preserves C^n
functions in a domain
at a point.
Composition by continuous linear maps on the left preserves C^n
functions on domains.
Composition by continuous linear maps on the left preserves C^n
functions.
Composition by continuous linear equivs on the left respects higher differentiability on domains.
Composition by continuous linear equivs on the left respects higher differentiability on domains.
If f
admits a Taylor series p
in a set s
, and g
is linear, then f β g
admits a Taylor
series in g β»ΒΉ' s
, whose k
-th term is given by p k (g vβ, ..., g vβ)
.
Composition by continuous linear maps on the right preserves C^n
functions at a point on
a domain.
Composition by continuous linear maps on the right preserves C^n
functions on domains.
Composition by continuous linear maps on the right preserves C^n
functions.
Composition by continuous linear equivs on the right respects higher differentiability at a point in a domain.
Composition by continuous linear equivs on the right respects higher differentiability on domains.
If two functions f
and g
admit Taylor series p
and q
in a set s
, then the cartesian
product of f
and g
admits the cartesian product of p
and q
as a Taylor series.
The cartesian product of C^n
functions at a point in a domain is C^n
.
The cartesian product of C^n
functions on domains is C^n
.
The cartesian product of C^n
functions at a point is C^n
.
The cartesian product of C^n
functions is C^n
.
Smoothness of functions f : E β Ξ i, F' i
#
Composition of C^n
functions #
We show that the composition of C^n
functions is C^n
. One way to prove it would be to write
the n
-th derivative of the composition (this is FaΓ di Bruno's formula) and check its continuity,
but this is very painful. Instead, we go for a simple inductive proof. Assume it is done for n
.
Then, to check it for n+1
, one needs to check that the derivative of g β f
is C^n
, i.e.,
that Dg(f x) β¬ Df(x)
is C^n
. The term Dg (f x)
is the composition of two C^n
functions, so
it is C^n
by the inductive assumption. The term Df(x)
is also C^n
. Then, the matrix
multiplication is the application of a bilinear map (which is C^β
, and therefore C^n
) to
x β¦ (Dg(f x), Df x)
. As the composition of two C^n
maps, it is again C^n
, and we are done.
There is a subtlety in this argument: we apply the inductive assumption to functions on other Banach
spaces. In maths, one would say: prove by induction over n
that, for all C^n
maps between all
pairs of Banach spaces, their composition is C^n
. In Lean, this is fine as long as the spaces
stay in the same universe. This is not the case in the above argument: if E
lives in universe u
and F
lives in universe v
, then linear maps from E
to F
(to which the derivative of f
belongs) is in universe max u v
. If one could quantify over finitely many universes, the above
proof would work fine, but this is not the case. One could still write the proof considering spaces
in any universe in u, v, w, max u v, max v w, max u v w
, but it would be extremely tedious and
lead to a lot of duplication. Instead, we formulate the above proof when all spaces live in the same
universe (where everything is fine), and then we deduce the general result by lifting all our spaces
to a common universe. We use the trick that any space H
is isomorphic through a continuous linear
equiv to continuous_multilinear_map (Ξ» (i : fin 0), E Γ F Γ G) H
to change the universe level,
and then argue that composing with such a linear equiv does not change the fact of being C^n
,
which we have already proved previously.
The composition of C^n
functions on domains is C^n
.
The composition of C^n
functions on domains is C^n
.
The composition of a C^n
function on a domain with a C^n
function is C^n
.
The composition of C^n
functions is C^n
.
The composition of C^n
functions at points in domains is C^n
.
The composition of C^n
functions at points in domains is C^n
.
The composition of C^n
functions at points is C^n
.
The bundled derivative of a C^{n+1}
function is C^n
.
The bundled derivative of a C^{n+1}
function is C^n
.
Sum of two functions #
The sum of two C^n
functions within a set at a point is C^n
within this set
at this point.
The sum of two C^n
functions at a point is C^n
at this point.
The sum of two C^n
functions is C^n
.
The sum of two C^n
functions on a domain is C^n
.
Negative #
The negative of a C^n
function within a domain at a point is C^n
within this domain at
this point.
The negative of a C^n
function at a point is C^n
at this point.
The negative of a C^n
function is C^n
.
The negative of a C^n
function on a domain is C^n
.
Subtraction #
The difference of two C^n
functions within a set at a point is C^n
within this set
at this point.
The difference of two C^n
functions at a point is C^n
at this point.
The difference of two C^n
functions on a domain is C^n
.
The difference of two C^n
functions is C^n
.
Sum of finitely many functions #
Product of two functions #
The product of two C^n
functions within a set at a point is C^n
within this set
at this point.
The product of two C^n
functions at a point is C^n
at this point.
The product of two C^n
functions on a domain is C^n
.
The product of two C^n
functions is C^n
.
Scalar multiplication #
The scalar multiplication of two C^n
functions within a set at a point is C^n
within this
set at this point.
The scalar multiplication of two C^n
functions at a point is C^n
at this point.
The scalar multiplication of two C^n
functions is C^n
.
The scalar multiplication of two C^n
functions on a domain is C^n
.
Cartesian product of two functions #
The product map of two C^n
functions within a set at a point is C^n
within the product set at the product point.
The product map of two C^n
functions on a set is C^n
on the product set.
The product map of two C^n
functions within a set at a point is C^n
within the product set at the product point.
The product map of two C^n
functions within a set at a point is C^n
within the product set at the product point.
The product map of two C^n
functions is C^n
.
Inversion in a complete normed algebra #
In a complete normed algebra, the operation of inversion is C^n
, for all n
, at each
invertible element. The proof is by induction, bootstrapping using an identity expressing the
derivative of inversion as a bilinear map of inversion itself.
Inversion of continuous linear maps between Banach spaces #
At a continuous linear equivalence e : E βL[π] F
between Banach spaces, the operation of
inversion is C^n
, for all n
.