Inverse function theorem and ContinuousLinearEquiv

Stream: mathlib4

[Yury G. Kudryashov]

WDYT about migrating the inverse function theorem and related results from assuming HasFDerivAt with a coercion of a ContinuousLinearEquiv to assuming (fderiv ..).IsInvertible?

[Yury G. Kudryashov]

We can also introduce StrictlyDifferentiableAt, so that we can assume it without providing an explicit derivative, then use fderiv to get the derivative.

[Sébastien Gouëzel]

I think it's a good idea: IsInvertible wasn't available at the time of writing the inverse function theorem, and it's less natural to have an assumption phrased in terms of a continuous linear equiv when fderiv is already around.

[Winston Yin (尹維晨)]

@A. has been working on #26985 which was ready to land. Please see #maths > Implicit function theorem in familiar form @ 💬 for context. This almost-ready PR is now in an uncertain state due to my own PR introducing IsContDiffImplicitAt.implicitFunctionData and due to this thread and #33611. They've been feeling dejected as a result, and I think we should coordinate the plan better amongst those interested.

[Yury G. Kudryashov]

In yet another related PR #33611, I introduce a parametric version of the theorem. I think that in the case when $\frac{\partial f}{\partial y}$ is an equivalence, my version (it requires surjectivity only) implies yours. OTOH, my version introduces the kernel of that derivative, which is trivial in your cases. I'm not sure what's the right design here.

[Yury G. Kudryashov]

Ah, I see that you already mention my PR.

[Yury G. Kudryashov]

I need the version from #33611 in full generality. I'm not 100% sure it conflicts with the other PRs, since it introduces the kernel and the projection onto this kernel into the mix.

[Yury G. Kudryashov]

I think that we should have different constructions of ImplicitFunctionData in Calculus/ImplicitFunction/*.lean.

[A.]

Yury G. Kudryashov said:

In yet another related PR #33611, I introduce a parametric version of the theorem. I think that in the case when $\frac{\partial f}{\partial y}$ is an equivalence, my version (it requires surjectivity only) implies yours. OTOH, my version introduces the kernel of that derivative, which is trivial in your cases. I'm not sure what's the right design here.

Yes I posted code in the other thread to demonstrate the possibility of deriving one implicitFunction from another.

[A.]

Yury G. Kudryashov said:

I think that we should have different constructions of ImplicitFunctionData in Calculus/ImplicitFunction/*.lean.

That’s fine. Probably easier that way.

[Yury G. Kudryashov]

If you move your version to a file there, then I can review&merge it. I think that there is no harm in having many versions there.

[Yury G. Kudryashov]

Please notify me here once you do it to minimize the delay on my side. Thank you!

[A.]

It's done. I created a new file Calculus/ImplicitFunction/OfProdDomain.lean for my own contribution. I also tried to git mv move @Winston Yin (尹維晨) 's Calculus/ImplicitContDiff.lean to Calculus/ImplicitFunction/ContDiffAt.lean but Github failed to track it and that screwed up the diff which seemed unhelpful. Perhaps Github will be able to track the move if it's done in its own special PR?

[A.]

The commit currently last in the branch had in fact passed CI but lost its green tick when I force pushed to revert the ContDiffAt file move commit.

[A.]

In the other thread @Winston Yin (尹維晨) suggested that maybe IsContDiffImplicitAt could be deprecated so I did that but it necessitated deleting quite a lot of ImplicitContDiff.lean which worried me. I sent him a message a couple of days ago.

[Yury G. Kudryashov]

Git detects file moves based on content. If you move & substantially change in the same PR, then it fails to detect the move.

[Yury G. Kudryashov]

In your PR, could you please move the implicit arguments to variable? @Winston Yin (尹維晨) Could you please have a look at the changes to your file?

[A.]

I hope I made the right move in replacing

def implicitFunctionOfProdDomain
    {u : E₁ × E₂} {f : E₁ × E₂ → F} {f₁ : E₁ →L[𝕜] F} {f₂ : E₂ ≃L[𝕜] F}
    (dfu : HasStrictFDerivAt f (f₁.coprod f₂) u) :
    E₁ → E₂ := ···

with

def implicitFunctionOfProdDomain
    {u : E₁ × E₂} {f : E₁ × E₂ → F} {f' : E₁ × E₂ →L[𝕜] F}
    (dfu : HasStrictFDerivAt f f' u) (if₂ : (f' ∘L .inr 𝕜 E₁ E₂).IsInvertible) :
    E₁ → E₂ := ···

?

My aim was to conform with your plans at the top of the thread.

[Yury G. Kudryashov]

Yes, thanks for doing this!

[Winston Yin (尹維晨)]

@A. These are good changes. I've left some review comments on your PR. Don't worry about deleting lots of stuff from ContDiffImplicit, as what you did subsumed those parts in a good way.