Current Status of the Stokes' theorem

Stream: mathlib4

[Yongxi Lin (Aaron)]

So many theorems in PDE and analysis (that I want to formalize) needs some version of the Stokes' theorem on a manifold (with corners). I know that there are people working on differential forms right now, but are there anything else I can do to accelerate this process of having the Stoke's theorem in Mathlib?

[Kevin Buzzard]

Can you state the theorem and PR it as proof_wanted?

[Yongxi Lin (Aaron)]

Actually I believe stating Stoke's theorem is harder than proving it. I don't think we are ready to state this theorem. We don't have the definition of differential forms in Mathlib yet, which requires the definition of tensor bundles. Do we have exterior derivatives (the d-operator in the Stokes' theorem)? Do we have a proof that the boundary of a manifold of dimension n is also a manifold of dimension n-1? I think we also need the definition of orientation on vector spaces and on manifolds.

[Michael Rothgang]

We have some of the ingredients already (either in mathlib or on a branch):

• we have the orientation of a module docs#Orientation, in particular of vector spaces
• #16239 has an almost correct definition of manifolds: it is wrong precisely for one-manifolds with boundary. There was a zulip discussion about fixing it (#Is there code for X? > Orientable Surface ); help with that is welcome. (It's on my list of items to return to, but not high priority right now.)

[Michael Rothgang]

I'd like to ask what you mean precisely by "the boundary of a n-manifold is an (n-1)-manifold": for instance, is the original manifold allowed to have corners? Note that mathlib's notion of a manifold says "manifold with boundary and corners of any order" (and is in fact slightly more general than this" --- so what you want to say is something like "M is a smooth manifold whose boundary is a smooth manifold without corners". #31351 does this.

[Michael Rothgang]

(It's not in mathlib yet for several reasons, the biggest one being that it's waiting on defining smooth immersions --- those are also PRed and will hopefully get merged this week.)

[Michael Rothgang]

This may seem pedantic --- my point is that mathlib-level generality exposes some genuine mathematical question that you need to take a stance on.

[Michael Rothgang]

Yury Kudryashov has formalised most of differential forms, without explicit language of tensor bundles. #30886 defines the exterior derivative of vector fields (on normed spaces). More work is in a dedicated repository, and gradually being PRed to mathlib.

[Michael Rothgang]

A PR adding docs#Orientation to the library overview is welcome, by the way: you want to modify https://github.com/leanprover-community/mathlib4/blob/master/docs/overview.yaml in a suitable way.

[Yongxi Lin (Aaron)]

Thank you Michael, I’ll take a look of these links first.

[David Michael Roberts]

Ironically, one of the reasons Bourbaki got started was to give a thorough treatment of Stokes' theorem from the gound up. The group accidentally reinvented 20th century mathematics first..... and I note the book on manifolds has not yet appeared, just the Fascicule des résultats, which, as the publisher's website says, "Il ne contient pas de démonstration."