Implicit function theorem

Stream: mathlib4

[Winston Yin (尹維晨)]

I'm surprised to see that the implicit function theorem in Mathlib.Analysis.Calculus.Implicit is not being used anywhere in mathlib. I'd like to develop this API more, as I need the existence of a $C^n$ implicit function. I'm seeing a bunch of todos in that file (including the one I'm trying to prove), so I want to make sure that @Yury G. Kudryashov or someone else does not have active plans for it before pressing ahead.

[Yury G. Kudryashov]

I need a $C^{r+\alpha}$ version for my current project.

[Yury G. Kudryashov]

I'm working on it right now, so please wait for a week or two, if it's convenient for you.

[Winston Yin (尹維晨)]

That's great to hear. Please let me know when there's a PR.

[Michael Rothgang]

Do you also need manifold versions? I have an old branch for the inverse function theorem for manifolds; the implicit function theorem would also be on my list of things.

[Winston Yin (尹維晨)]

Can we get the manifold version from the vector space version that Yury is developing?

[Winston Yin (尹維晨)]

Right now I just need the vector space version so I can prove that ODE solutions are smooth with respect to the initial condition.

[Michael Rothgang]

Indeed, that's how the proof should proceed.