Partial derivatives for function from Prod

Stream: mathlib4

[Yury G. Kudryashov]

In https://github.com/urkud/SardMoreira, I need fderiv Real (fun y => f (a, y)) b a lot, both in this form and as fderiv Real f (a, b) |>.comp (.inr _ _ _). AFAIR, @Patrick Massot needed partial derivatives of a similar kind for sphere eversion. Should we add them to Mathlib?

[Patrick Massot]

Indeed I used that in sphere eversion but @Floris van Doorn pushed a lot against it.

[Floris van Doorn]

Yeah, we definitely used that in sphere eversion.
I was worried about writing it as a new definition, which then requires a duplication of almost all of the fderiv API, and we have to copy this API for first partial derivative on Prod, second partial derivative on Prod, and the i-th partial derivative in (i : \i) -> E i.
It is not clear to me that this duplication is desirable. But if it would make working with partial derivatives a lot easier (does it?), then it is probably worth it.

[Yury G. Kudryashov]

For me, the main issue is that we have at least 3 ways to write this:

• fderiv Real (fun y => f (a, y)) b
• (fderiv Real f (a, b)).comp (.inl Real _ _)
• fderiv Real (f.curry a) b.

I'm OK if instead of introducing the definition, we just agree on which one is the normal form.

[Yury G. Kudryashov]

The last one has no counterpart for fderiv_1, so it's a bad candidate. The first two are equal for differentiable functions, but not for a function that's differentiable in y but not in (x, y).

[Yury G. Kudryashov]

In the SardMoreira project, I failed to choose one form, so had to rewrite back and forth here and there.

[Johan Commelin]

Did that experience teach you which one should be preferred?

[Yury G. Kudryashov]

Not yet. I was too busy rushing to the result.

[Yury G. Kudryashov]

I think that the first spelling makes more sense, because it works for functions that aren't differentiable in both variables.