Inner product are not that cheap

Stream: sphere eversion

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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.

[Patrick Massot]

@Oliver Nash

[Patrick Massot]

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

[Floris van Doorn]

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]

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

[Oliver Nash]

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

[Anatole Dedecker]

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]

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

[Oliver Nash]

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]

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]

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]

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

[Anatole Dedecker]

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]

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

[Sebastien Gouezel]

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]

Sébastien, this is precisely the topic.

[Patrick Massot]

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]

I mean for application in the sphere eversion project

[Patrick Massot]

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

[Sebastien Gouezel]

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]

Indeed this is what I'm suggesting.

[Oliver Nash]

I'll take this up now.

[Oliver Nash]

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]

Yes, please.

[Patrick Massot]

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

[Oliver Nash]

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

[Oliver Nash]

OK I've done that.

[Patrick Massot]

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

[Patrick Massot]

@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]

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

[Patrick Massot]

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]

@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]

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]

@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]

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

[Patrick Massot]

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

[Oliver Nash]

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]

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

[Oliver Nash]

Yes I see that.

[Patrick Massot]

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

[Oliver Nash]

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

[Patrick Massot]

That would be fantastic

[Patrick Massot]

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]

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.

[Patrick Massot]

Awesome

[Patrick Massot]

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

[Oliver Nash]

Understood.

[Patrick Massot]

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

[Oliver Nash]

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

[Sebastien Gouezel]

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]

@Oliver Nash :point_up:

[Oliver Nash]

I saw it :)

[Oliver Nash]

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]

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

[Patrick Massot]

Thanks

[Oliver Nash]

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

[Oliver Nash]

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]

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]

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

[Oliver Nash]

Agreed.

[Oliver Nash]

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

[Oliver Nash]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

I pushed.

[Oliver Nash]

We seem to have no graph at all now!

[Yaël Dillies]

No graph, no problem.

[Oliver Nash]

Patrick Massot said:

I had to add nonempty assumptions everywhere

Yes, I haven't forgotten about this. Hopefully I can resolve this tomorrow.

[Floris van Doorn]

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

[Patrick Massot]

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

[Patrick Massot]

I'm compiling again...

[Patrick Massot]

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

[Oliver Nash]

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]

The proof isn't marked \leanok

[Oliver Nash]

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]

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]

Great!