Stream: General

Topic: partial derivative

Anthony Bordg (Nov 01 2019 at 12:59):

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}$?

Anthony Bordg (Nov 07 2019 at 07:30):

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.

Fabian Immler (Nov 07 2019 at 15:01):

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.

Anthony Bordg (Nov 11 2019 at 16:39):

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

Last updated: Dec 21 2024 at 16:20 UTC