Just curious if there is a way to express the nth derivative of f or f^{(n)}(x) in Isabelle. Would this involve using something like "(f has_derivative f') (at x)" or would it involve DERIV or deriv?
I'm new to taking derivatives in Isabelle and I just want to show what the nth derivative of a real one-dimensional function is. For reference I included the following from Derivative.thy:
definition✐‹tag important› deriv :: "('a ⇒ 'a::real_normed_field) ⇒ 'a ⇒ 'a" where "deriv f x ≡ SOME D. DERIV f x :> D"
lemma DERIV_imp_deriv: "DERIV f x :> f' ⟹ deriv f x = f'" unfolding deriv_def by (metis some_equality DERIV_unique)
There's, of course, also the Deriv.thy where has_derivative is defined.
I'm inclined toward has_derivative but I don't have a strong reason, nor do I know if there is a general definition like for nth derivative.
If I were to define it myself I guess I would like it to have syntax similar to:
"(f has_nth_derivative n [lambda expression for nth derivative]) (at x)".
There are a lot of different kinds of derivatives in mathematics, and therefore there are also a lot of different kinds in Isabelle. Most of the time, it is convenient to actually work with a relation that establishes that there is a derivative and what the derivative is.
Here's an overview of the different things you might want to know. Hope it helps – feel free to reach out to me if you need any more assistance!
(f has_field_derivative D) (at x within A)
This is the notion that most people will probably use most of the type. This is the "normal" derivative that everyone knows from high school calculus. Here, one has f :: 'a :: real_normed_field ⇒ 'a and D :: 'a is a single number. Usually one has 'a = real or 'a = complex.
There is also an alias has_real_derivative which is just has_field_derivative specialised to reals; no idea why this exists.
(f has_vector_derivative D) (at x within A)
Here we have f :: (real ⇒ 'a :: real_normed_vector) and D :: 'b is a vector. You sometimes encounter this when you have functions real ⇒ complex or real ⇒ real × real, for example.
(f has_derivative D) (at x within A)
Here we have f :: 'a :: real_normed_vector ⇒ 'b :: real_normed_vector and D :: 'a ⇒ 'b is the unique linear function such that f(x+h) = f(x) + D(h) + o(h), i.e. the best possible local linear approximation to f at the point x. For a finitely-dimensional vector space, this is basically just the Jacobian matrix. This is the most general notion of derivative that we have, I think.
GDERIV f x :> D
Here we have f :: 'a :: real_inner ⇒ real and D :: 'a is a vector. This is the gradient (i.e. direction of steepest ascent). I don't think this is used very much in the library and I'm not sure how well-developed it is.
There is also some old legacy notation for these derivatives, e.g. DERIV f f x :> D instead of (f has_field_derivative D) (at x). It is less general than the other notation and is not used in new developments anymore, but it still shows up in the library because we haven't gotten rid of it yet everywhere.
The first three of these relations are in ascending order of generality. It is usually prudent to use the least general one that works for you. I.e. if you have a function real ⇒ real or complex ⇒ complex, just use has_field_derivative.
There is currently nothing like your has_nth_derivative notion, to my knowledge, although it would be easy to define one. However, as I see it, that would only work for has_field_derivative or has_vector_derivative: the derivative of a function real ⇒ real is again a function real ⇒ real and the derivative of a function real ⇒ real × real is again a function real ⇒ real × real; but the derivative of a function real × real ⇒ real is a function real × real ⇒ real × real, and the derivative of that would be a function that returns a matrix etc.
The at x within A bit above is actually a filter. This is used to specify where the derivative is being taken. The most basic thing you can write is just at x (which is an abbreviation for at x within UNIV). Then you just get the ‘normal’ derivative at a given point.
However, in some situations one might want to restrict the environment around x where the derivative is being taken. For that purpose, one can specify a set A. For example, for the left- and right-sided derivative, one can use at x within {..<x} and at x within {x<..}. Since these are used relatively often, there exist abbreviations at_left x and at_right x for them.
I haven't come across filters other than at x, at_left x, at_right x being used for derivatives, but they are more important for things like limits.
There are also predicates for simply asserting that a function is differentiable, but without saying what the derivative is:
(f field_differentiable F) (at x within A)(f differentiable F) (at x within A)These are for has_field_derivative/has_real_derivative and for has_vector_derivative/has_derivative, respectively. I for one have never really used them much since it's usually easier to just use the relations above.
I don't think we have anything like ‘n times differentiable’, although it would be relatively easy to define. There is a notion f C1_differentiable_on A and also f piecewise_C1_differentiable_on A, but this is mostly used for things like piecewise smooth paths and contour integration; I'm not sure how generally useful it is.
Sometimes it is also useful to have a derivative operator, i.e. something like d/dx in mathematics: a function that takes a function f and a point x and returns the derivative of f at the point x. For that purpose, we have these:
deriv f x
This is the unique function with the property (f has_field_derivative (deriv f x)) (at x). Of course, only provided that the derivative exists. If it does not exist, the value of deriv f x is unspecified.
vector_derivative f x
The same but for has_vector_derivative.
If you want the n-th derivative of f at x, you can write e.g. (deriv ^^ n) f x. Here, (^^) is an operator from the standard library that applies a function n times. However, I am not aware of there being a notion of a function being n-times differentiable in the standard library or the Archive of Formal Proofs, so I think this deriv ^^ n stuff is mostly used for complex analysis, where ‘differentiable once’ is the same as ‘arbitrarily often differentiable’.
A usual recipe for proving a derivative of a function is something like this:
lemma "x ≠ 0 ⟹ ((λx. exp (1 / x)) has_real_derivative (-exp (1/x) / x^2)) (at x)"
by (auto intro!: derivative_eq_intros simp: power2_eq_square field_simps)
Here, derivative_eq_intros is a dynamic rule collection of introduction rules that are set up in such a way that proving derivatives is relatively pain-free most of the time. Side conditions do arise (e.g. x ≠ 0 in this case), and if the automation cannot solve them by itself you might have to help it along. There are similar fact collections for limits and continuity (tendsto_intros/continuous_intros). Every time someone defines a new function, they should also provide such rules in order to make things go smoothly, and the rules should be as general as possible.
For complex functions in one variable (complex ⇒ complex), there exist some additional notions:
f holomorphic_on A: f is differentiable at every point in A
f analytic_on A: f is differentiable in some open superset of A (i.e. it has a convergent power series at every point in A)
f meromorphic_on A: roughly, like f analytic_on A but there might also be some poles. More precisely: f has a convergent Laurent series expansion at every point in A.