The reparametrization lemma

Stream: sphere eversion

[Patrick Massot]

Gromov's reparametrization lemma roughly says that if you have a loop $\gamma : \mathbb{S}^1 \to E$ for some real vector space $E$ and $x$ is in the interior of the convex hull of the image of $\gamma$ then one can reparametrize $\gamma$, ie precompose it will a diffeomorphism of $\mathbb{S}^1$ to ensure the average value of the new loop is $x$. In addition this can be done parametrically for any family of loops and target points. The proof uses smoothness of barycentric coordinates, smooth partitions of unity and integration. On paper the proof talks about measures but they are all measures admitting a smooth density with respect to the Lebesgue measure on $\mathbb{S}^1$ so measure theory is not really involved.

[Oliver Nash]

I've been slowly making progress on this lemma and pushing progress to https://github.com/leanprover-community/sphere-eversion/pull/51

The actual content of the result is that one can construct a smooth density function (representing a measure) with certain properties. Given this, one just uses the change-of-variables formula for an interval integral to get the actual result. The PR above (still very much WIP) does not address the content at all but just sets up the basic structure.

[Patrick Massot]

Sounds good! Don't hesitate to write documentation (module-level and declaration-level docstrings) as you go. Also you can push directly to master if you want. If you fear collisions with Floris then I suggests Floris creates a new file for exists_loop instead of having it in the reparametrization file where I originally put it.

[Patrick Massot]

It makes me think than when you'll be ready to go to the partition of unity argument you should probably talk with Floris about how he proved the extend_loop lemma

[Oliver Nash]

Thanks, my current plan is to squash the easy sorrys I've introduced so that this is reduced entirely to the existence of the density function. (This will probably take me a day or two.) Then I will either establish the local existence _or_ reduce the global existence to the local existence via the partition of unity arguement. Once I get there I'll pester Floris.

[Oliver Nash]

I'm happy to stay on this branch till I've reduce the problem to the existence of the density and then I may start working against master.

[Oliver Nash]

On second thought I think I might merge https://github.com/leanprover-community/sphere-eversion/pull/51 and start working off master now.

[Oliver Nash]

@Floris van Doorn this would just move exists_loops out of loops/reparameterization.lean and into a new file loops/exists.lean. Is that OK with you? Any other concerns etc?

[Floris van Doorn]

No concerns here. I haven't touched the relevant declarations recently.

[Patrick Massot]

Ok, I merged.

[Oliver Nash]

Excellent, thanks!

[Patrick Massot]

And I confirm the project still builds :grinning:

[Patrick Massot]

I see the reparametrization file still contains smooth_at but now everything should be smooth everywhere.

[Oliver Nash]

Yes, there is a bit of legacy which I'll efface shortly.

[Patrick Massot]

Also make sure you always keep https://leanprover-community.github.io/mathlib_docs/notes.html#continuity%20lemma%20statement in mind, it works really well.

[Oliver Nash]

Yes!

[Oliver Nash]

I was a total convert to this once I saw the comments Floris generously left at #10354 (and which I still must get back to some day).