2749 Implicit function theorem

Stream: PR reviews

[Yury G. Kudryashov]

Two out of three versions are ready for review. I'm not sure yet how should I formulate the prod case. E.g., should I use f : E × F → G or f : E → F → G? How should I say that f is differentiable in both variables and the derivative in the second variable is invertible? I don't like the way it is done now but can't come up with a better API.

[Yury G. Kudryashov]

#2749

[Heather Macbeth]

This is really exciting!

[Heather Macbeth]

The third (prod) version is what some people call the Rank Theorem, right?

[Heather Macbeth]

You have probably considered this, but could you phrase the invertibility of the derivative in the second variable by introducing a version of linearity of the right injection in the category of bounded linear maps?

[Yury G. Kudryashov]

What exactly do you suggest? Could you please just list arguments?

[Yury G. Kudryashov]

I learned all this in Russian and I don't know how people call this in English.

[Yury G. Kudryashov]

(except for what I read in Wikipedia and some textbooks)

[Heather Macbeth]

Instead of

(f'inv : G →L[𝕜] F)  (hf'l : ∀ y : F, f'inv (f' (0, y)) = y) (hf'r : ∀ z : G, f' (0, f'inv z) = z)

could you do

(hf' : is_linear_equiv (f' inr))

where inr is like linearity of the right injection in the category of bounded linear maps

[Heather Macbeth]

(the open mapping theorem would give that the inverse is also bounded linear, right?)

[Yury G. Kudryashov]

I see the following ways to formulate the prod version:

• (now in implicit.lean): f : E × F → G has derivative f', f'inv : G →L[k] F is an inverse for λ y, f (0, y);
• same with linear_map.comp instead of extensional equalities;
• (f : E → F → G) (f' : (E × F) →L[k] G) (f'y : F ≃L[k] G) (hf' : has_strict_fderiv_at (uncurry f) f'(x, y)) (hf'y : has_strict_fderiv (f x) f'y y);
• (f : E → F → G) (f' : (E × F) →L[k] G) (f'y : F ≃L[k] G) (hf' : has_strict_fderiv_at (uncurry f) f'(x, y)) (hf'y : f'.comp inr = f'y.

[Yury G. Kudryashov]

AFAIR, we don't have is_linear_equiv predicate.

[Heather Macbeth]

Yes, just seeing that.

[Heather Macbeth]

But can you write f' inr instead of λ y, f' (0, y) ?

[Yury G. Kudryashov]

I can write f'.comp inr, yes.

[Yury G. Kudryashov]

But I'm not sure whether I should ask for f'inv or f'y : F ≃L[k] G.

[Heather Macbeth]

I have seen that people who are more experienced with Lean often prefer the style $E \to F \to G$, but for me, the style $E\times F\to G$ seems better-adapted to this context.

[Heather Macbeth]

i.e., one is more likely to want to apply inverse function theorem on a map $E\times F\to G$, right?

[Heather Macbeth]

I don't know about
(f'y : F ≃L[k] G) (hf'y : f'.comp inr = f'y) vs
(f'inv : G →L[k] F) (hf'l : (f'.comp inr).comp f'inv = id) (hf'r : f'inv.comp (f'.comp inr) = id)
(or whatever the notation for the identity is)

[Heather Macbeth]

It seems like the former is more attractive, but would in the end be established by proving the latter?

[Yury G. Kudryashov]

My main concern about f'y style is that we ask for the same data (forward map of f'y) twice.

[Yury G. Kudryashov]

i.e., one is more likely to want to apply inverse function theorem on a map $E\times F\to G$, right?

Not if one defines all functions with two arguments as E → F → G.

[Heather Macbeth]

But often the domain will be an open subset of $E \times F$ which is not an exact product of an open subset of $E$ and an open subset of $F$?

[Heather Macbeth]

It seems a bit strange to think of the function $f(x,y,z)=(\sqrt{x^2+y^2}-2)^2+z^2-1$, which I would apply IFT to to produce a torus, as a map $\mathbb{R}^2\to C^\infty(\mathbb{R})$, defined by $(x,z)\mapsto (\sqrt{x^2+\cdot^2}-2)^2+z^2-1$. Maybe I am just not used to the Lean way of thinking yet ....

[Yury G. Kudryashov]

Unfortunately, this is not a $E \times F$ case.

[Yury G. Kudryashov]

Because $y$ is the middle variable and because most theorems about $\mathbb R^n$ use fin n → R.

[Yury G. Kudryashov]

This means that I probably should completely rewrite the prod case.

[Yury G. Kudryashov]

Or just drop it for now.

[Yury G. Kudryashov]

And see what we'll really need.

[Yury G. Kudryashov]

Added of_proj version which generalizes all others, removed prod_ for now.

[Patrick Massot]

Do we already have a version where we consider $f : E \to F$ and a isomorphism $\varphi : K \times H \simeq E$, unrelated to $f$, such that, under the appropriate assumptions, there is $g : K \to H$ such that, for $(k, h)$ in a neighborhood of $(k_0, h_0)$, $f\big(\varphi(k, h)\big) = f\big(\varphi(k_0, h_0)\big) \iff h = g(k)$? This appears to solve Heather's issue of "$y$ not being the last coordinate".

[Patrick Massot]

Anyway, I guess we could merge this (after adding some more docstrings) and wait for the real test: define submanifolds and prove $\mathbb S^n$ and $O_n(\mathbb R)$ are submanifolds.