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 with predicates ContDiffWithinAt
, ContDiffAt
, ContDiffOn
and
ContDiff
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, ContDiffOn
is not defined directly in terms of the
regularity of the specific choice iteratedFDerivWithin ๐ n f s
inside s
, but in terms of the
existence of a nice sequence of derivatives, expressed with a predicate
HasFTaylorSeriesUpToOn
defined in the file FTaylorSeries
.
We prove basic properties of these notions.
Main definitions and results #
Let f : E โ F
be a map between normed vector spaces over a nontrivially normed field ๐
.
ContDiff ๐ n f
: expresses thatf
isC^n
, i.e., it admits a Taylor series up to rankn
.ContDiffOn ๐ n f s
: expresses thatf
isC^n
ins
.ContDiffAt ๐ n f x
: expresses thatf
isC^n
aroundx
.ContDiffWithinAt ๐ n f s x
: expresses thatf
isC^n
aroundx
within the sets
.
In sets of unique differentiability, ContDiffOn ๐ n f s
can be expressed in terms of the
properties of iteratedFDerivWithin ๐ m f s
for m โค n
. In the whole space,
ContDiff ๐ n f
can be expressed in terms of the properties of iteratedFDeriv ๐ m f
for m โค n
.
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 iteratedFDerivWithin
) 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 ContDiffWithinAt
and ContDiffOn
.
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 ContDiffWithinAt ๐ 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).
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 โ
.
Tags #
derivative, differentiability, higher derivative, C^n
, multilinear, Taylor series, formal series
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
- ContDiffWithinAt ๐ n f s x = โ (m : โ), โm โค n โ โ u โ nhdsWithin x (insert x s), โ (p : E โ FormalMultilinearSeries ๐ E F), HasFTaylorSeriesUpToOn (โm) f p u
Instances For
Alias of ContDiffWithinAt.congr_of_mem
.
Alias of the reverse direction of contDiffWithinAt_insert
.
Alias of the forward direction of contDiffWithinAt_insert
.
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.
Alias of ContDiffWithinAt.differentiableWithinAt'
.
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
.
A version of contDiffWithinAt_succ_iff_hasFDerivWithinAt
where all derivatives
are taken within the same set.
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
- ContDiffOn ๐ n f s = โ x โ s, ContDiffWithinAt ๐ n f s x
Instances For
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
.
When a function is C^n
in a set s
of unique differentiability, it admits
ftaylorSeriesWithin ๐ 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 fderivWithin
) 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 fderivWithin
) 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^โ
.
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
- ContDiffAt ๐ n f x = ContDiffWithinAt ๐ n f Set.univ x
Instances For
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
- ContDiff ๐ n f = โ (p : E โ FormalMultilinearSeries ๐ E F), HasFTaylorSeriesUpTo n f p
Instances For
If f
has a Taylor series up to n
, then it is C^n
.
If a function is C^n
with n โฅ 1
, then it is differentiable.
A function is C^(n+1)
iff it has a C^n
derivative.
When a function is C^n
in a set s
of unique differentiability, it admits
ftaylorSeriesWithin ๐ f s
as a Taylor series up to order n
in s
.
If f
is C^n
then its m
-times iterated derivative is continuous for m โค n
.
If f
is C^n
then its m
-times iterated derivative is differentiable for m < n
.
A function is C^(n + 1)
if and only if it is differentiable,
and its derivative (formulated in terms of fderiv
) is C^n
.
A function is C^โ
if and only if it is differentiable,
and its derivative (formulated in terms of fderiv
) is C^โ
.
If a function is at least C^1
, its bundled derivative (mapping (x, v)
to Df(x) v
) is
continuous.