Support of partial derivative

[chenwydj]

Based on this page (https://leanprover-community.github.io/undergrad_todo.html), it seems the partial derivative (up to an arbitrary order) is not supported yet in mathlib4.

Can anyone brief the core bottleneck to implement the partial derivative into mathlib4/Lean4? If I want to do this, how challenging it would be?

Thank you!

[herostrat]

Hey, I found this zulip stream with infos that could help you
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Partial.20derivatives

[chenwydj]

@herostrat Thank you very much!!

[chenwydj]

Hi @herostrat! Based on the zulip chat, I think lineDeriv is the most appropriate way for partial derivatives.

However, I'm not sure if mathlib4 supports integration over multi-variable functions.

[grunweg]

To reflect what was said on zulip: yes, mathlib has integration over multi-variable functions.