Zulip Chat Archive

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.

Oliver Nash (Dec 14 2021 at 18:23):

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

leanprover-community / mathlib