Stream: General

Topic: partial derivative


view this post on Zulip 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:RnRf:\mathbb{R}^n \rightarrow \mathbb{R}?

view this post on Zulip 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 Rn\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.

view this post on Zulip 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.

view this post on Zulip Anthony Bordg (Nov 11 2019 at 16:39):

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


Last updated: Aug 15 2022 at 04:16 UTC