Using iterated_fderiv

Stream: new members

[Zhangir Azerbayev]

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?

[Heather Macbeth]

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

[Zhangir Azerbayev]

Thank you @Heather Macbeth .

[Patrick Massot]

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

[Patrick Massot]

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

[Heather Macbeth]

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

[Alex J. Best]

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

[Victor Tsynkov]

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.

[Sebastien Gouezel]

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).

[Mario Carneiro]

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

[Mario Carneiro]

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

[Victor Tsynkov]

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!

[Victor Tsynkov]

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.

[Jalex Stark]

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

[Sebastien Gouezel]

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.