Zulip Chat Archive

Stream: new members

Topic: Using iterated_fderiv


view this post on Zulip Zhangir Azerbayev (Jun 30 2020 at 20:53):

I'm trying to state that the second derivative is symmetric (or a special case of this, by mathlib standards).

variable f :  ×   

theorem partial_symm (h : times_cont_diff  2 f) (p :  × ) :
 v w :  × , iterated_fderiv  2 f p (v, w) = iterated_fderiv  2 f p (w, v) := sorry

I'm getting an error saying that my (v, w) should have type Π (i : fin 2), (λ (i : fin 2), ℝ × ℝ) i. What is this type, and how do I construct a term of that type?

view this post on Zulip Heather Macbeth (Jun 30 2020 at 21:18):

With the caveat that I have never used these libraries, I might suggest

variables {E : Type*} [normed_group E] [normed_space  E]
variable f : E  

theorem partial_symm (h : times_cont_diff  2 f) (p : E)
  (σ : equiv.perm (fin 2)) (v : (fin 2)  E) :
  iterated_fderiv  2 f p (v  σ) = iterated_fderiv  2 f p v

view this post on Zulip Zhangir Azerbayev (Jun 30 2020 at 22:54):

Thank you @Heather Macbeth .

view this post on Zulip Patrick Massot (Jun 30 2020 at 23:03):

Just to make sure things are clear: Heather gave you a more general statement than what you wanted, since E could have any dimension (even infinite). What you tried to state is:

import analysis.calculus.times_cont_diff

def swap : fin 2  fin 2 := λ i, if i = 0 then 1 else 0

variable f :  ×   

theorem partial_symm (h : times_cont_diff  2 f) (p :  × ) :
 v : fin 2   × , iterated_fderiv  2 f p v = iterated_fderiv  2 f p (v  swap) :=
sorry

view this post on Zulip Patrick Massot (Jun 30 2020 at 23:05):

I also used swap instead of a general permutation of {0,1}\{0, 1\} as Heather did, but this is of course a trivial change, contrary to going from dimension 2 to arbitrary dimension.

view this post on Zulip Heather Macbeth (Jun 30 2020 at 23:11):

I used a general permutation to conceal the fact that I did not know how write down swap!

view this post on Zulip Alex J. Best (Jul 01 2020 at 00:03):

There is swap as a perm also in data.equiv.basic, which might have some useful lemmas proved about it.
So you can do

import data.equiv.basic
import analysis.calculus.times_cont_diff
open equiv

variable f :  ×   

theorem partial_symm (h : times_cont_diff  2 f) (p :  × ) :
 v : fin 2   × , iterated_fderiv  2 f p v = iterated_fderiv  2 f p (v  swap 0 1) :=
sorry

view this post on Zulip Victor Tsynkov (Jul 01 2020 at 10:44):

Not sure I understand the arguments in iterated_fderiv and there aren't many comments in mathlib. Please help me clarify: in iterated_fderiv ℝ 2 f p v the point where the derivative is evaluated is p ? If that is true, why not rather use permutations on finset.range n to indicate what derivative is taken. To make a connection between the present choice and usual notation, what is v going to be for example if one needs d^2/dx^2 versus d^2/dxdy? Sorry if I miss something obvious here.

view this post on Zulip Sebastien Gouezel (Jul 01 2020 at 10:51):

The derivative in mathlib is the general notion of Fréchet derivative, i.e., a linear map approximating the original map around a point. So, we are not talking of derivatives in a specific directions, but rather in all directions simultaneously. The derivative in direction a is fderiv k f p a. In the same way, the iterated derivative is a multilinear map, taking all directions into account at the same time. So, if you want to compute the second derivative in directions a and b, you write iterated_fderiv k 2 f p v, where v = (a, b) (except that it is seen as a function from fin 2 to your space E, instead of an element of E x E, as this is the point of view that generalizes well to higher derivatives).

view this post on Zulip Mario Carneiro (Jul 01 2020 at 10:53):

There is a discussion of the meanings of the arguments in the header comment of https://leanprover-community.github.io/mathlib_docs/analysis/calculus/times_cont_diff.html

view this post on Zulip Mario Carneiro (Jul 01 2020 at 10:55):

So the answer to the question is that v should be (0 -> (1, 0), 1 -> (1, 0)) for d^2/dx^2 and (0 -> (1, 0), 1 -> (0, 1)) for d^2/dxdy, where (0 -> a, 1 -> b) is the function on fin 2 taking 0 to a and 1 to b

view this post on Zulip Victor Tsynkov (Jul 01 2020 at 10:58):

Mario Carneiro said:

So the answer to the question is that v should be (0 -> (1, 0), 1 -> (1, 0)) for d^2/dx^2 and (0 -> (1, 0), 1 -> (0, 1)) for d^2/dxdy, where (0 -> a, 1 -> b) is the function on fin 2 taking 0 to a and 1 to b

This is the part I was missing. Thank you!

view this post on Zulip Victor Tsynkov (Jul 03 2020 at 09:56):

Mario Carneiro said:

There is a discussion of the meanings of the arguments in the header comment of https://leanprover-community.github.io/mathlib_docs/analysis/calculus/times_cont_diff.html

Maybe it's because I'm not a mathematician, but it seems to me that exactly the part that is more difficult to understand, about what the map v is, is missing from those explanations.

view this post on Zulip Jalex Stark (Jul 03 2020 at 14:01):

reading mathlib is not supposed to be an efficient way to learn multivariable calculus

view this post on Zulip Sebastien Gouezel (Jul 03 2020 at 15:33):

Jalex Stark said:

reading mathlib is not supposed to be an efficient way to learn multivariable calculus

I don't read it this way. Instead, I see that we are missing a whole API around partial derivatives, and we will definitely need to add it some day, because this is the way many people approach and use calculus.


Last updated: May 10 2021 at 19:16 UTC