Smoothness of barycentric coordinates (Lemma 1.7)

Stream: sphere eversion

[Patrick Massot]

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]

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]

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

[Floris van Doorn]

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?

[Patrick Massot]

sure

[Patrick Massot]

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

[Patrick Massot]

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

[Oliver Nash]

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]

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]

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

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

[Oliver Nash]

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]

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]

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]

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]

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]

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]

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]

Ok, I guess this is ready to merge then?

[Oliver Nash]

I think so!

[Patrick Massot]

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]

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