More versions of the Implicit Function Theorem

Stream: mathlib4

[Yury G. Kudryashov]

For https://github.com/urkud/SardMoreira, I needed two new custom constructors for docs#ImplicitFunctionData. Have you seen these kinds of the Implicit Function Theorem in other context? #xy: should I treat them as implementation details or something that deserves a proper API when I upstream the code to Mathlib?

Implicit function theorem for maps with non-surjective differential

In this case, we choose a projection onto LinearMap.range (fderiv K f a), then apply the usual theorem to the composition of this projection with our map. As a result, instead of locally conjugating our map to Prod.fst, we locally conjugate it to fun (x, y) => (x, g x y) for some function with dg/dy = 0.

This conjugation appears as the first step in most (all?) proofs of variants of the Sard's theorem, but I don't know if it appears in any other context. If yes, then I'll think how to extend the docs#ImplicitFunctionData structure to accomodate for this use case. If no, then I'll just add a custom constructor and prove exactly what I need for Sard's theorem (that's what I already have in my repo).

Implicit function preserving the first coordinate

Given a function f : E × F → G with surjective df/dy, we can find an implicit function that preserves the first coordinate, see https://urkud.github.io/SardMoreira/docs/SardMoreira/Chart.html#Moreira2001.chartImplicitData (see source for details) for the case G = Real. Probably, this can be seen as a parametric version of the theorem, so it has greater chances of being useful in other context. How would you call the corresponding constructor to ImplicitFunctionData?

[Yury G. Kudryashov]

CC: @Sébastien Gouëzel @Patrick Massot @Floris van Doorn