second partial derivative test

Stream: mathlib4

[Johannes Riesterer]

Hello,

is there a formalisation of https://en.wikipedia.org/wiki/Second_partial_derivative_test

thanks in advance

Johannes

[Yury G. Kudryashov]

No

[Patrick Massot]

You should search zulip for second derivative test.

[Yury G. Kudryashov]

(AFAIK)

[Patrick Massot]

I am sure there was a recent conversation about it.

[Johannes Riesterer]

ok thanks for your help

[Bjørn Kjos-Hanssen]

I have a new pull request for it the single-variable version: #18266 I formalized exactly the proof given in Wikipedia (which is better than e.g. what is found in common textbooks like Stewart and Thomas).

[Patrick Massot]

@Bjørn Kjos-Hanssen ☀️ could you clarify whether this is still a draft or ready for review?

[Bjørn Kjos-Hanssen]

I'll say ready for review at this point.

[Johannes Riesterer]

this is for one dimensional functions , or? Is there also a proof for higher dimensions?

[Bjørn Kjos-Hanssen]

Yes, it is for 1-dimensional functions over ℝ. It's starting from monotoneOn_of_deriv_nonneg which is at that level of generality. It would be great if someone generalizes it further.

[Johannes Riesterer]

Ok, thank you. I will try to do it but i don't know if i will proceed. seems challanging somehow :-) .

[Johannes Riesterer]

maybe if you can help here and there would be great....

[Bjørn Kjos-Hanssen]

I agree it seems challenging! To get started, there are some Zulip threads about partial derivatives.