Understanding Symmetric Derivative

Stream: general

[Max Bobbin]

Hello,
I was hoping I could get some help understanding what the notation of #second_derivative_symmetric. I am trying to formalize Maxwell's relations (https://en.wikipedia.org/wiki/Maxwell_relations#Derivation) which rely on the idea of the symmetric second derivative. Am I understanding correctly that when it says (f'' v) w = (f'' w) vit means d^2 f / (dv dw) =d^2 f / (dw dv) ?

[Eric Wieser]

(note it's docs# not # to link to things in mathlib)

[Patrick Massot]

It means $d^2f(x)(v, w) = d^2f(x)(w, v)$.

[Patrick Massot]

I don't know what your notation means. If you want to specialize to $E = \R^n$ then you can use the canonical basis $(e_1, \dots, e_n)$ and choose $v = e_i$ and $w = e_j$ to get $\frac{\partial^2 f}{\partial x_i\partial x_j}(x) = \frac{\partial^2 f}{\partial x_j\partial x_i}(x)$.

[Patrick Massot]

But if you think only in terms of $\R^n$ and partial derivatives instead of general vector spaces and total derivatives then you will have a very hard time using differential calculus in mathlib.

[Max Bobbin]

Eric Wieser said:

(note it's docs# not # to link to things in mathlib)

Thank you! Sorry, I'm still trying to learn all the notation.

[Max Bobbin]

Patrick Massot said:

But if you think only in terms of $\R^n$ and partial derivatives instead of general vector spaces and total derivatives then you will have a very hard time using differential calculus in mathlib.

Thank you! This is helpful and brings up a couple of other questions I have. First, apologies for the messed up notation. I was trying to write out the second partial derivative of f. Basically what you wrote in your second reply except w = x_i and v = x_j. However, you second reply does answer my first question which is understanding the notation. I'm not a mathematician so I'm used to the simple partial derivative. So when we write this in lean(f'' v) w , if I'm understanding correctly, f'' is a function that takes in real numbers each through a linear map and outputs a real number (assuming E and F are real numbers). Then v and w are elements of the vector x. If x is a vector of length n, then there are n possible first derivatives and then we plug in two elements from the vector of x to get a specific second derivative?

For your third part: As I said above, I'm not a mathematician, so I'm familiar with the simple stuff of derivatives and partials. When you say total derivatives, do you mean that the frechet derivative of a function at x fderiv(R f x) is the total derivative of f and could be represented as a finite sum of first partial derivatives of length equal to the length of x?

I can send a document of my written out proof to give more context of how I was thinking about going about my proof and seeing how I could implement it in Lean

Thank you so much for all your help, I really appreciate it!

[Max Bobbin]

Maxwells-Relations-General-Proof-Outline.pdf
Here is a brief outline of what I have been trying to show in Lean. Please let me know if there's any ambiguity, I tried to make sure to define everything for a math proof but I may have missed stuff