iterated mfderiv

Stream: Is there code for X?

[Chris Birkbeck]

Do we have iterated derivatives between manifolds? We seem to have iterated_fderiv and iterated_deriv but I can't find anything else. Also, while I'm here, is there a deriv version of iterated_fderiv_tsum? (I can't find them, but I'm also very bad at finding things in mathlib).

[Sebastien Gouezel]

Iterated derivatives of maps between manifolds don't really make sense in general (and that's why we don't have them in mathlib): if f is a function between two manifolds, then the second derivative of f at a point x (as a bilinear map on the tangent space at x) is canonical only when the first derivative of f at x vanishes. If you want a general definition, you will need a connection on the tangent bundle (probably with some good properties).

[Chris Birkbeck]

OK fair enough, that's a good point. I guess I was thinking of this for the specific case I have in mind, where I have a function on the complex upper half plane (to the complex numbers) and I want to take its iterated derivative, but I cant use iterated_deriv or iterated_fderiv since my domain isnt a field

[Chris Birkbeck]

I can do the trick of extending by zero, but thats annoying to work with

[Floris van Doorn]

It's usually harder to work with a partial function than a function extended by 0. For this reason, we extend many functions in mathlib with 0, even though they "should" be partial functions (operations like division, integrals, derivatives, ...).

[Chris Birkbeck]

When I first defined modular forms, in order to say they were holomorphic I just extended by zero outside the upper half plane and used 'differentiable_on', but this wasn't very nice to use, since I kept having to ensure I was on the upper half plane for things to work and morally it was the wrong definition to use. Which is why the current definition uses 'mdifferentiable'.

In this case I just want to take an identity on the upper half plane and differentiate it n-times. So maybe it won't be that bad extending by zero, but it feels like that sort of thing that one could do with 'mderiv' in this setting.