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-th derivative of a function at the (n-1)-th derivative of the 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. We also define a version iterated_fderiv_within relative to a domain, as well as predicates times_cont_diff 𝕜 n f and times_cont_diff_on 𝕜 n f s saying that the function is C^n, respectively in the whole space or on the set s.
We prove basic properties of these notions.
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[𝕜]. We define this space inductively, call it iterated_continuous_linear_map 𝕜 n E F, and denote it by E [×n]→L[𝕜] F. We can define it inductively either from the left (i.e., saying that the (n+1)-th space S_{n+1} is E →L[𝕜] S_n) or from the right (i.e., saying that the (n+1)-th space associated to F, denoted by S_{n+1} (F), is equal to S_n (E →L[𝕜] F)). For proofs, it turns out to 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). In other words, one could define the (n+1)-th derivative either as the derivative of the n-th derivative, or as the n-th derivative of the derivative. We use the latter definition.
A difficulty is related to universes: the first and second spaces in the sequence, for n=0 and 1, are F and E →L[𝕜] F. If E has universe u and F has universe v, then the first one lives in v and the second one in max v u. Since they should live in the same universe (as all the other spaces in the construction), it means that at the 0-th step we should not use F, but ulift it to universe max v u. But we should also ulift its vector space structure and its normed space structure. This can certainly be done, but I decided it was not worth it for now. Therefore, the definition is only made when E and F live in the same universe.
Regarding the definition of C^n functions, there are two equivalent definitions:
Therefore, we give (and use) both definitions, named respectively times_cont_diff_rec and times_cont_diff (as well as relativized versions on a set). We show that they are equivalent. The first one is mainly auxiliary: in applications, one should always use times_cont_diff (but the proofs below use heavily the equivalence to show that times_cont_diff is well behaved).
derivative, differentiability, higher derivative, C^n
The space iterated_continuous_linear_map 𝕜 n E F is the space E →L[𝕜] (E →L[𝕜] (E ... F)...))), defined inductively over n. This is the space to which the n-th derivative of a function naturally belongs. It is only defined when E and F live in the same universe.
Define by induction a normed group structure on the space of iterated continuous linear maps. To avoid resetI in the statement, use the @ version with all parameters. As the equation compiler chokes on this one, we use the nat.rec_on version.
Define by induction a normed space structure on the space of iterated continuous linear maps. To avoid resetI in the statement, use the @ version with all parameters. As the equation compiler chokes on this one, we use the nat.rec_on version.
Explicit normed group structure on the space of iterated continuous linear maps.
Explicit normed space structure on the space of iterated continuous linear maps.
The n-th derivative of a function, defined inductively by saying that the (n+1)-th derivative of f is the n-th derivative of the derivative of f.
The n-th derivative of a function along a set, defined inductively by saying that the (n+1)-th derivative of f is the n-th derivative of the derivative of f.
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.
Auxiliary definition defining C^n functions by induction over n. In applications, use times_cont_diff instead.
Auxiliary definition defining C^n functions on a set by induction over n. In applications, use times_cont_diff_on instead.
A function is C^n on a set, for n : with_top ℕ, if its derivatives of order at most n are all well defined and continuous.
The two definitions of C^n functions on domains, directly in terms of continuity of all derivatives, or by induction, are equivalent.
If a function is at least C^1 on a set, it is differentiable there.
If a function is at least C^1, its bundled derivative (mapping (x, v) to Df(x) v) is continuous.
Being C^n is a local property.
A function is C^n, for n : with_top ℕ, if its derivatives of order at most n are all well defined and continuous.
Constants are C^∞.
Linear functions are C^∞.
The first projection in a product is C^∞.
The second projection in a product is C^∞.
The identity is C^∞.
Bilinear functions are C^∞.
Composition by bounded linear maps preserves C^n functions on domains.
Composition by bounded linear maps preserves C^n functions.
The cartesian product of C^n functions on domains is C^n.
The cartesian product of C^n functions is C^n.
The composition of C^n functions on domains is C^n.
The composition of a C^n function on domain with a C^n function is C^n.
The composition of C^n functions 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.
The sum of two C^n functions on a domain is C^n.
The sum of two C^n functions is C^n.
The negative of a C^n function on a domain is C^n.
The negative of a C^n function is C^n.
The difference of two C^n functions on a domain is C^n.
The difference of two C^n functions is C^n.