## Stream: sphere eversion

### Topic: Inner product are not that cheap

#### Patrick Massot (Aug 29 2022 at 17:50):

We've finally hit the point where assuming inner product spaces everywhere this was locally more convenient strikes back.

#### Patrick Massot (Aug 29 2022 at 17:51):

The problem is that we don't have product inner product spaces. See this topic

#### Patrick Massot (Aug 29 2022 at 17:53):

When reducing to the non-parametric case we use a product manifold. This is fine if there are no inner product spaces around. But then the localization work uses inner product spaces everywhere. If I understood correctly at that time, this was simply convenient when building diffeomorphisms between balls and whole spaces.

#### Patrick Massot (Aug 29 2022 at 17:54):

If this is indeed the only reason then the correct fix is clearly to go back to global/smooth_embedding.lean and work harder there.

@Oliver Nash

#### Patrick Massot (Aug 29 2022 at 17:55):

And then we'll need to propagate that change to localization_data.lean, but I hope this is easy

#### Floris van Doorn (Aug 29 2022 at 18:13):

I feel that it will be easier to do as much as we can using inner product spaces, and then only at the end transform it to a statement about normed spaces (possibly using the fact that all norms are equivalent on a finite dimensional vector space). Otherwise you are dealing with 2 different norms when dealing e.g. with docs#cont_diff_bump.

#### Patrick Massot (Aug 29 2022 at 19:13):

Yes, we probably need to state and prove wrapper lemmas that use the current version.

#### Oliver Nash (Aug 29 2022 at 19:32):

I'll think about this first thing tomorrow morning but my first instance is to attempt what Floris has suggested.

#### Anatole Dedecker (Aug 29 2022 at 19:37):

Floris van Doorn said:

possibly using the fact that all norms are equivalent on a finite dimensional vector space

Will docs#linear_equiv.to_continuous_linear_equiv be enough or do you really need the inequality version of equivalent norms ?

#### Oliver Nash (Aug 29 2022 at 19:37):

Actually I'm not 100% convinced equivalence of norms is strong enough: we may care about more than the topology.

#### Oliver Nash (Aug 29 2022 at 19:38):

I'll have to think about it in the morning but filling in missing API for inner_product_space might be the thing to do.

#### Anatole Dedecker (Aug 29 2022 at 19:42):

Oliver Nash said:

Actually I'm not 100% convinced equivalence of norms is strong enough: we may care about more than the topology.

Yes but continuous linear maps are smooth so having a docs#continuous_linear_equiv should be enough to preserve differentiability, right ?

#### Oliver Nash (Aug 29 2022 at 19:46):

Perhaps I'm being stupid but here's an example of what concerns me. Consider the map defined in docs#homeomorph_unit_ball and suppose we have the l1 norm. Surely it's not smooth?

#### Oliver Nash (Aug 29 2022 at 19:47):

Unfortunately I must close my laptop for the evening now. I'll take this up tomorrow.

#### Anatole Dedecker (Aug 29 2022 at 19:50):

Oliver Nash said:

Perhaps I'm being stupid but here's an example of what concerns me. Consider the map defined in docs#homeomorph_unit_ball and suppose we have the l1 norm. Surely it's not smooth?

It isn't in general, but it should be in finite dimension right? Or am I missing something stupid? EDIT: I am, the ball is not the same anymore

#### Patrick Massot (Aug 29 2022 at 19:51):

The norm itself isn't smooth, even away from zero.

#### Sebastien Gouezel (Aug 29 2022 at 19:51):

This specific map doesn't look like it's smooth. But in finite dimension there is always a diffeomorphism between the unit ball and the whole space (this is not completely trivial!)

#### Patrick Massot (Aug 29 2022 at 19:52):

SΓ©bastien, this is precisely the topic.

#### Patrick Massot (Aug 29 2022 at 19:52):

Actually we only care about the fact that points have a neighborhood basis made of sets that are diffeomorphic to the whole space.

#### Patrick Massot (Aug 29 2022 at 19:52):

I mean for application in the sphere eversion project

#### Patrick Massot (Aug 29 2022 at 19:53):

So this is probably the statement that we should be aiming for.

#### Sebastien Gouezel (Aug 29 2022 at 19:53):

This is much easier: use the one from the inner product space, composed with a continuous linear equiv coming from the fact that norms are equivalent.

#### Patrick Massot (Aug 29 2022 at 19:54):

Indeed this is what I'm suggesting.

#### Oliver Nash (Aug 30 2022 at 08:05):

I'll take this up now.

#### Oliver Nash (Aug 30 2022 at 08:10):

Would it help to push a commit immediately which restates lem:nice_atlas and lem:ex_localisation so that they demand normed_space instead of inner_product_space but with sorried proofs until I finish.?

#### Patrick Massot (Aug 30 2022 at 09:53):

I've been trapped in admin all morning but I hope I'll have lean time this afternoon.

#### Oliver Nash (Aug 30 2022 at 09:56):

OK I'll push up a sorried commit relaxing inner_product_space to normed_space in the next few minutes.

#### Oliver Nash (Aug 30 2022 at 10:01):

OK I've done that.

#### Patrick Massot (Aug 30 2022 at 12:12):

As I feared, we are also hitting issues with product manifolds.

#### Patrick Massot (Aug 30 2022 at 12:13):

@Sebastien Gouezel am I right to think that the moment we write smooth_manifold_with_corners π(β, E) M we decide we won't ever take a product?

#### Patrick Massot (Aug 30 2022 at 12:14):

We should be using docs#model_with_corners.boundaryless , right?

#### Patrick Massot (Aug 30 2022 at 12:15):

I mean that if we have smooth_manifold_with_corners π(β, E) M and smooth_manifold_with_corners π(β, E') M' then we won't have smooth_manifold_with_corners π(β, E Γ E') (M Γ M'), right?

#### Patrick Massot (Aug 30 2022 at 12:18):

@Oliver Nash I'm pretty sure this is exactly where boundaryless was invented so we need that assumption in the localization_data file

#### Sebastien Gouezel (Aug 30 2022 at 12:19):

Yes, I think that's the current situation. Concrete manifolds are typically constructed using π(β, E), but abstract theorems should be stated assuming boundaryless because that's stable under products.

If you see ways to improve on this, don't hesitate to do it! You should have played enough with the manifolds to see the weak points of the current implementation and possible improvements, hopefully.

#### Oliver Nash (Aug 30 2022 at 12:23):

@Patrick Massot So I should change the localisation data API so that it demands hypotheses of the form {I : model_with_corners β E E} [I.boundaryless] rather than π(β, E) ?

#### Patrick Massot (Aug 30 2022 at 12:25):

I'm not sure whether this is enough or whether you need {I : model_with_corners β E H}. @Sebastien Gouezel ?

#### Patrick Massot (Aug 30 2022 at 12:26):

The test case is exactly we want to apply the localisation API to a product.

#### Oliver Nash (Aug 30 2022 at 12:26):

I expect I can settle that myself once I attempt it. I've literally just seen this boundaryless for the first time now. I think I get the idea.

#### Patrick Massot (Aug 30 2022 at 12:26):

This all comes from the goal to deduce the parametric theorem from the unparametric one applied to a product.

Yes I see that.

#### Patrick Massot (Aug 30 2022 at 12:27):

While you're at it, please also make E an explicit argument in std_localisation_data

#### Oliver Nash (Aug 30 2022 at 12:28):

I suppose I should pause the work to close this sorry and take this up now instead?

#### Patrick Massot (Aug 30 2022 at 12:28):

That would be fantastic

#### Patrick Massot (Aug 30 2022 at 12:29):

Because we need to make sure lemmas fit together before working on proving them (since we are sure the proofs we are talking about will work in the end)

#### Oliver Nash (Aug 30 2022 at 12:29):

OK. I'll take five minutes to tidy up and push what I have and then I'll pivot to seeing if I can adjust the std_localisation_data API along these lines.

Awesome

#### Patrick Massot (Aug 30 2022 at 12:30):

Don't hesitate to push with sorries if the statements are ok and you checked the lemma applies to a product manifold.

Understood.

#### Patrick Massot (Aug 30 2022 at 12:31):

I'm sorry I haven't though more carefully about all this, but this is all specific to formalization.

#### Oliver Nash (Aug 30 2022 at 12:31):

Ah sure, this sort of thing is part of the point the project!

#### Sebastien Gouezel (Aug 30 2022 at 12:35):

Patrick Massot said:

I'm not sure whether this is enough or whether you need {I : model_with_corners β E H}. Sebastien Gouezel ?

Definitely {I : model_with_corners β E H}.

#### Patrick Massot (Aug 30 2022 at 12:38):

@Oliver Nash :point_up:

I saw it :)

#### Oliver Nash (Aug 30 2022 at 12:44):

OK I've pushed a commit parking the work on closing the sorry introduced by relaxing inner_product_space to normed_space and I'll start looking into fixing the API for std_localisation_data now.

#### Oliver Nash (Aug 30 2022 at 13:29):

This is going to take a while even though it's totally straightforward. I hope to finish this today but I cannot guarantee.

Thanks

#### Oliver Nash (Aug 30 2022 at 13:57):

OK I've just pushed a commit which I think should give you the API you need for std_localisation_data

#### Oliver Nash (Aug 30 2022 at 13:58):

Unfortunately the various quick revisions means that the code quality in smooth_embedding.lean is getting quite low but for now this is a secondary concern.

#### Oliver Nash (Aug 30 2022 at 14:00):

Assuming what I've done for std_localisation_data is correct, I suppose I might as well make corresponding changes for nice_update_of_eq_outside_compact (even though in this case I think we could get away with what we have).

#### Patrick Massot (Aug 30 2022 at 14:01):

It would be morally correct to do it everywhere but it shouldn't be needed

Agreed.

#### Oliver Nash (Aug 30 2022 at 14:02):

Maybe I'll leave that lemma alone then and see about de-sorrying the file smooth_embedding.lean.

#### Oliver Nash (Aug 30 2022 at 14:04):

I'm going to take a short break to listen to some Wodehouse while I walk in the sun. Please let me know if what I've done for std_localisation_data does not look right.

#### Patrick Massot (Aug 30 2022 at 14:13):

Sorry, I was finishing some "almost done" proof. I'll look right now

#### Patrick Massot (Aug 30 2022 at 14:44):

I can confirm we are back on track (but with more sorries and less green in the graph :sad:)

#### Patrick Massot (Aug 30 2022 at 14:46):

I had to add nonempty assumptions everywhere but I haven't proved the 2-sphere is nonempty since I hope we'll get rid of this assumption in the main theorem.

I pushed.

#### Oliver Nash (Aug 30 2022 at 14:49):

We seem to have no graph at all now!

#### YaΓ«l Dillies (Aug 30 2022 at 14:49):

No graph, no problem.

#### Oliver Nash (Aug 30 2022 at 14:50):

Patrick Massot said:

I had to add nonempty assumptions everywhere

#### Floris van Doorn (Aug 30 2022 at 14:52):

Woohoo, all nodes in the graph are green! (at least until the graph is non-empty again.)

#### Patrick Massot (Aug 30 2022 at 14:53):

This was the usual suspect: I had an outdated leanblueprint plugin on this computer

#### Patrick Massot (Aug 30 2022 at 14:53):

I'm compiling again...

#### Patrick Massot (Aug 30 2022 at 14:57):

We no longer have a graph where all nodes are green so we should get back to work.

#### Oliver Nash (Aug 30 2022 at 14:57):

It doesn't matter but I don't understand why lem:open_ample_immersion did not turn green. I must add the leanok to lem:open_ample_immersion.

#### Patrick Massot (Aug 30 2022 at 14:58):

The proof isn't marked \leanok

#### Oliver Nash (Sep 01 2022 at 15:40):

I've just pushed a commit which finishes the proof of nice_atlas (again). This time it:

• Holds for any normed_space rather than just inner_product_spaces
• Works for any boundaryless model_with_corners rather than just model_with_corners_self

#### Oliver Nash (Sep 01 2022 at 15:43):

Because I bootstrap the result for normed_spaces up from the easier result for inner_product_spaces there is a funny dance at the end which was amazingly easy thanks to a great API that we have for Euclidean spaces, bases, and equivalence of norms in finite dimensions. It starts here: https://github.com/leanprover-community/sphere-eversion/blob/4efaab178715ab819997010c4c8b3907f518ea8e/src/to_mathlib/analysis/normed_space/misc.lean#L165

#### Patrick Massot (Sep 01 2022 at 16:15):

Great!

Last updated: Dec 20 2023 at 11:08 UTC