## Stream: sphere eversion

### Topic: Smoothness of barycentric coordinates (Lemma 1.7)

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

In order to continuously construct surrounding families, it is important that barycentric coordinates smoothly depend both on the target points and one the affine basis. This Lemma 1.7.

It seems plausible that Oliver will work on this after completing Lemma 1.6. But help is welcome. There are intermediate lemmas to prove, most probably including some smoothness properties for determinants of families of vectors (one should check what is already in mathlib about differentiation of multi-linear maps).

Note that the statement oscillated in the blueprint. I started with a strong enough statement but later I weakened it to a continuity statement because I had in mind only one use of the lemma whereas there are two.

It would be nice to state this lemma in order to allow a proof of the reparametrization lemma.

#### Oliver Nash (Oct 08 2021 at 15:36):

I haven't thought seriously about this lemma yet but I plan to do so early next week by which time I will (hopefully) have finished with Lemma 1.6.

#### Oliver Nash (Oct 26 2021 at 17:00):

I will finally start working on this lemma, now called Lemma 1.8, later this evening.

#### Floris van Doorn (Nov 29 2021 at 18:30):

Am I correct in assuming that both the blueprint and the formal statement of Lemma 1.8 should have $\sum_{i=0}^dw_i(y,q)=1$ in the conclusion?

sure

#### Patrick Massot (Nov 29 2021 at 18:39):

It doesn't cost much in the proof since $w_0$ is defined as $1 - \sum_{i=1}^d w_i$

#### Patrick Massot (Nov 29 2021 at 18:39):

But indeed I forgot to put it in the conclusion (and then I blindly formalized the statement...)

#### Oliver Nash (Nov 29 2021 at 19:12):

I should have mentioned here that I’m on holiday in the Canaries this week so I’m afraid I can’t comment on detail. I can say that the proof of 1.8 that I’ve been assembling will just be a union of general results I’ve slowly added to Mathlib so changes like the one proposed above make no material difference.

#### Oliver Nash (Dec 09 2021 at 21:42):

After two weeks of interruption I was finally able to resume work on this today. I'm getting close enough that I've created a PR for it. It's not yet sorry-free and not yet ready for review but it will get there https://github.com/leanprover-community/sphere-eversion/pull/41

#### Heather Macbeth (Dec 09 2021 at 21:48):

@Oliver Nash Did you know that the smoothness of matrix inversion is already in mathlib? Not quite in that name, but check out docs#times_cont_diff_at_map_inverse

#### Oliver Nash (Dec 10 2021 at 09:52):

@Heather Macbeth Thank you, I did not know this. It would be very gratifying to factor what we need through this result.

#### Oliver Nash (Dec 10 2021 at 09:54):

I've actually already finished a low-tech proof of what this would do for me but I'll return to see if I can use docs#times_cont_diff_at_map_inverse once I've killed off my remaining (downstream) sorrys.

#### Oliver Nash (Dec 11 2021 at 22:56):

Oliver Nash said:

After two weeks of interruption I was finally able to resume work on this today. I'm getting close enough that I've created a PR for it. It's not yet sorry-free and not yet ready for review but it will get there https://github.com/leanprover-community/sphere-eversion/pull/41

I got annoyed waiting for myself to write a nice proof so this evening I just bashed out a horrendous monstrosity. I'll have to return to this next week since what I have is too horrible to merge but we do at least have the result without any sorrys now.

#### Oliver Nash (Dec 13 2021 at 16:16):

I spent several hours today tidying up https://github.com/leanprover-community/sphere-eversion/pull/41 and it may now be mergeable. In particular I claim the proof Lemma 1.7 is now reasonable

#### Oliver Nash (Dec 13 2021 at 16:17):

On the other hand, I have not really tried to combat some grossness in the proposed new file src/loops/smooth_barycentric.lean. I'm happy to polish this up too but I thought I'd request feedback first since we might be OK to leave the code there in a not-amazing-but-OK state and just move on to other things.

#### Patrick Massot (Dec 13 2021 at 20:26):

The results in that new file seem general enough to belong to mathlib, but some proofs should probably be generalized from determinant to multilinear maps. I would say we can keep it like this and move on. With a bit of luck someone will need the generalized version before we come back to it. Could you add comments explaining the parts that you don't like and what could be done?

#### Patrick Massot (Dec 13 2021 at 20:27):

You can also update the blueprint if Lemma 1.7 does not depend on any sorry (and maybe change the TeX proof a bit if you followed a different path).

#### Oliver Nash (Dec 14 2021 at 15:16):

I updated the Blueprint proof in this commit of the lemma and added some comments about what I don't like and what could be done in this commit.

#### Patrick Massot (Dec 14 2021 at 16:14):

Ok, I guess this is ready to merge then?

I think so!

#### Patrick Massot (Dec 14 2021 at 18:09):

This lemma is now merged! It's a really nice milestone. It should be the end of elementary geometry in the project (modulo finishing Anatole's ampleness lemma).

#### Patrick Massot (Dec 14 2021 at 18:11):

Floris is working on ∃_surrounding_loops, so the next lemma in line the reparametrization lemma!

Last updated: Dec 20 2023 at 11:08 UTC