Using localInverse

Stream: new members

[Michael Novak]

Using the theorem for the derivative of the inverse function in the 1D case gives us the derivative of the so called localInverse, but how can I use it to talk about the derivative of the normal inverse function? I couldn't find any theorems that relate localInverse to other functions.

[David Loeffler]

The problem is that "the" inverse function isn't generally a well-defined thing.

In situations where an inverse function does exist, maybe docs#HasDerivAt.of_local_left_inverse is what you're looking for? This allows you to supply a function f, a second function g, and a proof that f (g y) = y for y in a neighbourhood of some point a, and get back a relation between the derivative of g at a, and the derivative of f at g a.

[Michael Novak]

Thank you very much! I think this might indeed be what I'm looking for.