Higher differentiability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 cont_diff_within_at, cont_diff_at, cont_diff_on and 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, 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 nontrivially normed field 𝕜.

• has_ftaylor_series_up_to n f p: expresses that the formal multilinear series p is a sequence of iterated derivatives of f, up to the n-th term (where n is a natural number or ∞).
• has_ftaylor_series_up_to_on n f p s: same thing, but inside a set s. The notion of derivative is now taken inside s. In particular, derivatives don't have to be unique.
• cont_diff 𝕜 n f: expresses that f is C^n, i.e., it admits a Taylor series up to rank n.
• cont_diff_on 𝕜 n f s: expresses that f is C^n in s.
• cont_diff_at 𝕜 n f x: expresses that f is C^n around x.
• cont_diff_within_at 𝕜 n f s x: expresses that f is C^n around x within the set s.
• iterated_fderiv_within 𝕜 n f s x is an n-th derivative of f over the field 𝕜 on the set s at the point x. It is a continuous multilinear map from E^n to F, defined as a derivative within s of iterated_fderiv_within 𝕜 (n-1) f s if one exists, and 0 otherwise.
• iterated_fderiv 𝕜 n f x is the n-th derivative of f over the field 𝕜 at the point x. It is a continuous multilinear map from E^n to F, defined as a derivative of iterated_fderiv 𝕜 (n-1) f if one exists, and 0 otherwise.

In sets of unique differentiability, 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, cont_diff 𝕜 n f can be expressed in terms of the properties of iterated_fderiv 𝕜 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 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 cont_diff_within_at and 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 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 ∞.

Tags #

derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series

Functions with a Taylor series on a domain #

Smooth functions within a set around a point #

Smooth functions within a set #

Iterated derivative within a set #