## Stream: sphere eversion

### Topic: Corrugations estimates

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

This is the very heart of the whole proof. Lemma 2.3 explains how the loops of chapter 1 allow to improve the derivative of a map in some direction almost without touching the derivative in a complementary hyperplane. This is pure calculus using continuity and differentiation of parametric integrals. There is a tiny beginning of proof in corrugation.lean. Progress will be possible as soon as the parametric integral stuff is stated.

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

Note that the corrugation estimates lemma is also slowly moving. @Oliver Nash if you are tired of linear algebra and want to do calculus instead then I could write sorried statements trying to open access to the next lemma which is the main inductive step.

#### Oliver Nash (Dec 14 2021 at 18:20):

Thanks for the advice, I might well do that.

#### Oliver Nash (Dec 14 2021 at 18:21):

However first I want to take care of bunch of other loose ends (dangling PRs) that I've let slide for quite a while given my focus on SE.

#### Oliver Nash (Dec 14 2021 at 18:22):

As soon as I pick a new target, I'll announce it somewhere in this stream.

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

Ok, hopefully I can prepare things in the mean time. The end of this week will be complicated but the beginning of next week should be good.

Sounds good!

#### Patrick Massot (Dec 22 2021 at 17:52):

The main corrugation estimates are now done!

#### Patrick Massot (Dec 22 2021 at 17:53):

It took me a while to polish them because I reorganized a lot of things in the middle of finishing them. I also modified the blueprint statement to get something more precise and closer to the formulation in Lean.

#### Oliver Nash (Dec 22 2021 at 17:55):

Wow, this is super!

Last updated: Dec 20 2023 at 11:08 UTC