Project update

Stream: sphere eversion

[Patrick Massot]

The corrugation estimates that I finished are the central computations of the project, the heart of the calculus/integration side of the project. The elementary geometry side is already one, mostly by Oliver and Anatole, and the topology/gluing side is well under way thanks to Floris's work.

[Patrick Massot]

The differential geometry side is still up for grab.

[Patrick Massot]

Heather, I'm looking at you.

[Patrick Massot]

Section 3.1 is completely independent from all this.

[Heather Macbeth]

Ok, ok, ok :)

[Heather Macbeth]

I can't do anything for at least a couple of weeks yet, I'm afraid. So feel free to preempt me. But I guess the first step is to define smooth vector bundle?

[Patrick Massot]

I must admit I don't even know where we are with vector bundles.

[Heather Macbeth]

There is the definition of topological vector bundle:
https://github.com/leanprover-community/mathlib/blob/master/src/topology/vector_bundle.lean
and then a bunch of unmerged PRs developing their further theory.

[Heather Macbeth]

#7803,#8154, #8295, #8545

[Patrick Massot]

So yes, we need smooth vector bundle.

[Patrick Massot]

Now I have a lot of definition and statements writing to do. We have almost unsorried everything that was stated in the project (the notable exception being the reparametrization lemma).

[Johan Commelin]

This sounds like great progress. Wonderful!

[Patrick Massot]

Yes, we're seeing great progress. Having Oliver and Floris working on it helps tremendously. And also we needed a lot of foundational work on linear algebra, topology and integration, so for a very long time it really looked like the project wasn't moving at all.

[Patrick Massot]

I cleanup a lot of files yesterday and today, moving stuff to the to_mathlib folder. The real project files are pretty short.

[Patrick Massot]

I just pushed a rather large batch of new definitions and statements in local.relation and local.h-principle. This includes 23 new sorries for people interested in contributing to this project. The ones in the first file are meant to be easy. As usual there could be mistakes in those definitions and statements, don't hesitate to ask if something doesn't seem to make sense, especially if it seems inconsistent with the blueprint.

[Patrick Massot]

With this new step, Chapters 1 and 2 are entirely stated. But Chapter 3 (about manifolds) is still completely untouched.

[Patrick Massot]

My next personal goal is to unsorry the definition of the improvement step, hooking chapter 1 into chapter 2. This will unlock working on the sorries of local.h_principle.