In Derivative.thy there are the partial derivatives of a function of 2 variables (see for instance the proposition `has_derivative_partialsI`

). Has Isabelle ready-made code for the partial derivatives of a function of n variables, for instance with $f:\mathbb{R}^n \rightarrow \mathbb{R}$?

I can do it as follows.

locale partial_deriv = fixes n:: nat and f:: "real list ⇒ real" and l:: "real list" assumes length_list: "length l = n" and Dxif: "∀i<n.∃Dxif.∀x. ((λxi. f (list_update l i xi)) has_derivative Dxif) (at x within UNIV)"

Since there is no dependent type $\mathbb{R}^n$ in Isabelle, the code above is a bit convoluted, but it does the trick. I would be interested if someone knows a better way to do it.

I once did the following (https://www.isa-afp.org/browser_info/current/AFP/Ordinary_Differential_Equations/ODE_Auxiliarities.html):

lemma has_derivative_partials_euclidean_convexI: fixes f::"'a::euclidean_space ⇒ 'b::real_normed_vector" assumes f': "⋀i x xi. i ∈ Basis ⟹ (∀j∈Basis. x ∙ j ∈ X j) ⟹ xi = x ∙ i ⟹ ((λp. f (x + (p - x ∙ i) *⇩R i)) has_vector_derivative f' i x) (at xi within X i)" assumes df_cont: "⋀i. i ∈ Basis ⟹ (f' i ⤏ (f' i x)) (at x within {x. ∀j∈Basis. x ∙ j ∈ X j})" assumes "⋀i. i ∈ Basis ⟹ x ∙ i ∈ X i" assumes "⋀i. i ∈ Basis ⟹ convex (X i)" shows "(f has_derivative (λh. ∑j∈Basis. (h ∙ j) *⇩R f' j x)) (at x within {x. ∀j∈Basis. x ∙ j ∈ X j})" (is "_ (at x within ?S)")

It could make sense to define something like "(has_partial_derivative)" and develop a library about it.

But in my experience, it often makes sense to avoid dealing with partial derivatives and just use the total derivative:

Often, one assumes continuous partial derivatives, and then the above theorem shows that you get a total derivative from that, so why not use the easier (to work with) total derivative in the first place.

Thank you Fabian for pointing out the possible use of euclidean space here.

Last updated: Dec 07 2023 at 08:19 UTC