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 that f is C^n, i.e., it admits a Taylor series up to rank n.
ContDiffOn 𝕜 n f s: expresses that f is C^n in s.
ContDiffAt 𝕜 n f x: expresses that f is C^n around x.
ContDiffWithinAt 𝕜 n f s x: expresses that f is C^n around x within the set s.

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

Higher differentiability #

Main definitions and results #

Implementation notes #

Definition of C^n functions in domains #

Notations #

Tags #

Smooth functions within a set around a point #

Smooth functions within a set #

Smooth functions at a point #

Smooth functions #

Definition of `C^n` functions in domains #