## Stream: sphere eversion

### Topic: The reparametrization lemma

#### Patrick Massot (Oct 08 2021 at 15:35):

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 (Feb 22 2022 at 15:01):

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 (Feb 22 2022 at 15:48):

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 (Feb 22 2022 at 15:50):

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 (Feb 22 2022 at 16:19):

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 (Feb 22 2022 at 16:20):

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 (Feb 22 2022 at 18:04):

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 (Feb 22 2022 at 18:04):

@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 (Feb 22 2022 at 18:19):

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

Ok, I merged.

#### Oliver Nash (Feb 22 2022 at 18:23):

Excellent, thanks!

#### Patrick Massot (Feb 22 2022 at 18:23):

And I confirm the project still builds :grinning:

#### Patrick Massot (Feb 22 2022 at 18:26):

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

#### Oliver Nash (Feb 22 2022 at 18:26):

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

#### Patrick Massot (Feb 22 2022 at 18:27):

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

Yes!

#### Oliver Nash (Feb 22 2022 at 18:32):

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).

Last updated: Dec 20 2023 at 11:08 UTC