# Zulip Chat Archive

## Stream: new members

### Topic: Using iterated_fderiv

#### 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?

#### 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
```

#### Zhangir Azerbayev (Jun 30 2020 at 22:54):

Thank you @Heather Macbeth .

#### 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
```

#### Patrick Massot (Jun 30 2020 at 23:05):

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 (Jun 30 2020 at 23:11):

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

!

#### 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
```

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

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

#### 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

#### 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

#### 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!

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

#### Jalex Stark (Jul 03 2020 at 14:01):

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

#### 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