manifolds

Stream: maths

[Hoang Le Truong]

I have the definition of manifold over a normed field in Lean. You can see it in the following link
https://github.com/truonghoangle/manifolds
If you do not mind, please can you give me advice about it, special name of function or section and approach way to the definition of tangent bundle.

[Johan Commelin]

Are you aware of the fact that @Sebastien Gouezel is also working on manifolds? Did you coordinate with him?

[Hoang Le Truong]

When I began with manifold, I did not known @Sebastien Gouezel is also working on manifolds. Now I will contact him.

[Johan Commelin]

Here is one discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Multiple.20differentiability

[Johan Commelin]

Here is another one that might be relevant: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/out_param

[Johan Commelin]

@Hoang Le Truong Here is another attempt by Patrick: https://github.com/PatrickMassot/lean-differential-topology

[Hoang Le Truong]

Thank @Johan Commelin for your information

[Sebastien Gouezel]

The current state of thingsI have done on manifolds is in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/basic.lean. I am going for a more general approach, that would also encompass manifolds with boundaries, or manifolds with corners, or Thurston's (G,X) structures, but essentially the basic definitions are the same as yours, i.e., an atlas such that the changes of charts belong to some class of maps (called a groupoid, as in the fundamental textbook of Kobayashi and Nomizu). What I have done so far:

• extended the material on derivatives, to get access to a convenient API (PRed in #966)
• defined local equivalences, just like you do except I use genuine functions instead of pfuns, to avoid defining yet another notion of derivatives (and I don't care what the functions do outside of their domains and codomains), and defined a basic interface for them (in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/local_equiv.lean). The fact that this is a good choice has been questioned by several people on Zulip, who encouraged me to use pfuns as you do, but for now it seems to go rather smoothly -- I need to develop the library further to see what the advantages and drawbacks are.
• defined C^n functions, and proved basic properties (invariance under addition, composition, and so on), in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/times_cont_diff.lean
• defined general manifolds based on groupoids. As well as diffeomorphisms (for the groupoid structure), and proved that the inverse or the composition of two diffeomorphisms is a diffeomorphism (this is not so obvious) in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/basic.lean. Specialized to smooth manifolds, for which I am now defining the tangent space.

My goal would be to go up to the Whitney embedding theorem (any smooth real manifold embeds in R^N for large enough N), which is a non-trivial theorem, to stress-test the definitions and the interface.

[Sebastien Gouezel]

One important point in library-building, I think, is that writing down definitions is not enough: you need to prove theorems, to see how definitions work out well or not, and what interface you need for the proofs. For instance, the first statement I settled to prove is that the composition of diffeomorphisms is a diffeomorphism. This showed me that I needed to implement a serious interface to local equivs, that now takes over 800 lines. And now defining the tangent space shows me gaps in this interface, that I will have to fill.

[Hoang Le Truong]

My goal would be to go up to the Hodge theorem. I also think that the definition is right through the proof of the theorems. For instance about tangent bundle, we have three ways to give the definition. Moreover, for complex manifold, we have three tangent bundle. I am struggling between approachable approach on complex, real number and general ways.

[Johan Commelin]

Do you want to state the Hodge theorem or also prove it?

[Johan Commelin]

Either of them would be fantastic!

[Sebastien Gouezel]

I am going for a general way (over any field), as follows: let charts x be the set of all charts around x. If e and e' are such charts, they yield a linear map from E to E, the derivative of e' o e^{-1}. Take the quotient of (charts x) × E under these identifications, this gives the tangent space. Hopefully, this should be easily generalizable to define exterior or symmetric products of the tangent bundle, opening the way to Riemannian metrics and to differential forms. But before doing the general case, I will stick to tangent spaces for now.

[Sebastien Gouezel]

Another definition would be to choose one chart around each point, and only use this one to define the tangent space. This avoid taking a quotient, but it is less canonical. I will have to do it at some point, though, because I will want the derivative of a map to be a bounded linear map between tangent spaces, and for this I need a normed space structure on the tangent space, for which there is no canonical choice.

[Patrick Massot]

I think there will be painful points in any case, the only question is whether the API will be able to hide them

[Sebastien Gouezel]

Yes, it is definitely going to be nontrivial.

[Hoang Le Truong]

@Johan Commelin I want to prove it but first step is to give the statement of the Hodge theorem

[Hoang Le Truong]

@Sebastien Gouezel are you think how definition of tangent space via derivations is good

[Hoang Le Truong]

@Patrick Massot can you explain detaily about whether the API will be able to hide them

[Sebastien Gouezel]

Definition of tangent space via derivations is very nice, but as far as I remember proofs that it behaves well require localizing functions around the point, and while this works well over R this creates problems over C where you don't have partitions of unity. And this construction is really specific to tangent spaces, while the stupid approach using equivalence classes of vectors should be generalizable to other vector bundles.

[Kevin Buzzard]

One important point in library-building, I think, is that writing down definitions is not enough: you need to prove theorems, to see how definitions work out well or not, and what interface you need for the proofs.

Tom Hales' project does not need proofs, so for this project one might find that writing down definitions is in many cases enough. If the goal is just to formalise statements of theorems then this might provide far fewer demands on the definition-builder.

[Hoang Le Truong]

With complex maifold we have real tangent bundle, complexified tangent bundle and holomorphic tangent bundle. In fact, we begin with real tangent bundle. So I don't understand what the problems over C is.

[Sebastien Gouezel]

You don't need to separate the real case and the complex case: there is a definition which works for both at the same time. So, to minimize work, it is probably better to use this one.

[Hoang Le Truong]

@Sebastien Gouezel I read carefully the definition of very general manifold. It is very nice. I have question:What is the definition of submanifold? Is the definition of submanifold dependent on model space?

[Neil Strickland]

Can you comment on why your local_equiv α β actually involves maps defined on all of α and β, rather than just the indicated subsets? This seems to be asking for trouble later. Among other things, it means that an empty type cannot have a local equivalence with a nonempty one, which is a problem if α and β arise naturally as subtypes of something else. Can you not use maps α → roption β and β → roption α or something like that? That way, the eq_on_source thing would become unnecessary.

[Sebastien Gouezel]

There are pros and cons to both approaches, i.e. (1): functions defined everywhere, but you don't care about the values outside of the source, and (2): roption, i.e., really kill the values outside of source.

In (1), if functions are equal on the source but different outside, then they are not equal, while you want to think of them as the same function. That's the role of eq_on_source, which is definitely an annoyance.

In (2), your function does not take values in the right space, and this calls for trouble. For instance, if you want to define the derivative of a function f : M -> M' where M and M' are manifolds, what you do is write f in charts, i.e., consider e' o f o e^{-1} where e and e' are charts around xand f x, and then you differentiate. With the roption approach, what you get is a function from E to roption E', so you can not define the derivative as the limit of (f(x+hv)-f(x))/h when htends to 0 (or an equivalent definition using small o) as it does not make sense to subtract elements of roption E', or to divide them by a scalar. So, you would need to extend many algebraic definitions to roption, or to restrict your function to some suitable set and play some nontrivial dance there.

I have the feeling that (2) will create many more concrete problems than (1). Most of the time, we don't care at all about equality of charts, we just use one given chart and that's it. While having to reproject your function back to Eto do some algebraic manipulation happens all the time. That's why I went for (1). But you are not the first person to voice concerns about this choice.

[Mario Carneiro]

You can define the derivative when the function is defined on an open set around the target point

[Mario Carneiro]

the little o definition with a filter for roption functions actually makes this pretty painless

[Mario Carneiro]

Jeremy and I worked it out a while ago

[Sebastien Gouezel]

You can definitely work it out. The same for continuity: there is already an API for continuity of partial functions, crafted by Jeremy. Except that it is some amount of work. Then when you want to talk about C^k functions, or analytic functions, or Besov functions, or whatever, and even if you have already done it for functions you will need to spend some time to define again the same notions for partial functions (with a well developed API if you want these notions to be usable). This is completely avoided by the approach (1), at the expense of the mild annoyance that equality between charts (which is essentially never used) is not the right notion.

[Mario Carneiro]

You don't want to lift every algebraic operation to roption exactly; you use the monad structure for that

[Mario Carneiro]

I'm not sure it's true to say it's completely avoided; instead you have to build an API for eq_on_bla and local_equiv and such. It's moving the work elsewhere

[Sebastien Gouezel]

I think in any case you will need to build an API for local_equiv. Even with partial functions, you will need to bundle two partial functions which are inverse to each other on their respective domains, and see how they compose and so on.

[Mario Carneiro]

no, that's equiv of subtypes

[Sebastien Gouezel]

Not really, because you want to be able to compose them even when when the target of the first one is not the source of the second one, by automatically taking the intersection of the domains. Composition of roption-valued functions does that automatically, but composition of equivs of subtypes does not.

[Mario Carneiro]

that's true. I guess you need to forget about the domains in the types in your case

[Mario Carneiro]

still I like the fact that using subtypes gives you topology for free... can roption do the same?

[Hoang Le Truong]

2) With the roption approach, I change a function E → roption E to function E → E by
def ext_by_zero(f : β →. α) (z:β) : α := if h:z ∈ f.dom then f.fn z h else 0
When we only work on x ∈ f.dom

[Hoang Le Truong]

Fisrt I work only with complex field and definition of manifold ℂ β local_equiv α β also work only funtions α → β. But we can change ℂ to any field k. When we work on field 𝔽₁ then empty function joint theory as absorbing element. Therefore I choose local_equiv α β include empty function

[Mario Carneiro]

I think the natural topology on roption A is the one-point compactification

[Mario Carneiro]

@Johannes Hölzl Do you know a way to do the topology of roption A with filters?

[Sebastien Gouezel]

I am still puzzled by my question that started this thread: how come a simpinvocation can create a ghost duplication of some objects, that disappears if one adds a rw just before, in https://github.com/sgouezel/mathlib/blob/f6d6492e7a8b892b4a22fb010fb12d1a4695d38a/src/geometry/manifolds/mderiv.lean#L604. Any hint on what is going on would be welcome.

[Reid Barton]

I wonder whether it would be useful to introduce germs of functions here (a "germ of a function f : X -> Y at x : X" is a neighborhood N of x together with a function N -> Y, modulo the relation that two germs agree if they have a common restriction to a smaller neighborhood). Notions like continuity, derivatives and all higher-order information is local--meaning it only depends on the germ.

[Reid Barton]

I guess it's better to only allow continuous functions, so that you can compose germs.

[Neil Strickland]

I think that it would be best if the foundations of manifolds used sheaves explicitly. If you don't do it explicitly then I think you end up duplicating a lot of the ideas anyway. Many of the most popular manifolds are algebraic varieties, and you make the interface with algebraic geometry much smoother if you use similar foundations. In that context, germs become very natural.

[Johan Commelin]

This has been discussed, but Patrick and Sebastien both said that this is not a good strategy for the general theory of manifolds. I trust their judgment.

[Kevin Buzzard]

Maybe for them, many of the most popular manifolds are not algebraic varieties.

[Sebastien Gouezel]

For me, elliptic curves are surfaces, and they are all the same :)

[Kevin Buzzard]

yeah that's not a good sign

[Kevin Buzzard]

I spent many years studying their moduli spaces!

[Kevin Buzzard]

For you it's the one point set.

[Johan Commelin]

@Sebastien Gouezel Aren't you interested in varying an almost complex structure on that unique elliptic curve?

[Sebastien Gouezel]

Of course I am joking. Teichmüller space is one of my favorite playgrounds.

[Sebastien Gouezel]

I wonder whether it would be useful to introduce germs of functions here (a "germ of a function f : X -> Y at x : X" is a neighborhood N of x together with a function N -> Y, modulo the relation that two germs agree if they have a common restriction to a smaller neighborhood). Notions like continuity, derivatives and all higher-order information is local--meaning it only depends on the germ.

I considered this, or at least introducting predicates locally_equal_at and locally_equal_within_at. Finally, I decided that it does not help much to simplify other arguments, so I haven't introduced the definition, but I am still using it implicitely at some places, see for instance https://github.com/sgouezel/mathlib/blob/6d693c310ab036171dabadcf8924e5bc15ec8054/src/geometry/manifolds/mderiv.lean#L552

[Patrick Massot]

I think that it would be best if the foundations of manifolds used sheaves explicitly. If you don't do it explicitly then I think you end up duplicating a lot of the ideas anyway. Many of the most popular manifolds are algebraic varieties, and you make the interface with algebraic geometry much smoother if you use similar foundations. In that context, germs become very natural.

We should have a FAQ dedicated only to this question. This is an old algebraic geometry people fantasy relying on no mathematical content as far as we've seen. Pretending to define smooth manifold as ringed spaces only adds definitions without buying anything, and then the idea stops completely as soon as you want extra structure on your manifold.

[Neil Strickland]

What extra structure do you have in mind? You can certainly do vector bundles, tangent bundles, metrics, symplectic structures, connections, curvature, exterior derivatives, almost complex structures very naturally from the ringed space viewpoint.

[Sebastien Gouezel]

Triangulations. Flows. Much of Riemannian geometry (for instance geodesic flow or Jacobi fields). Connected sums. Knots and surgery. Open book structure in contact manifolds. Thurston's (G,X) structures. PDEs. Perelman's geometrization theorem (yes, we're aiming high :). And many other things that a true differential geometer would know much better than me (I am more into dynamical systems and probability theory).

Understand me well: I am not saying that none of this can be formalized in terms of ringed spaces. However, when doing anything about these concepts I think it would only come in the way and make things more complicated to state and prove.

[Scott Morrison]

There's also the pragmatic point that there are no written sources for anything on Sebastien's list written using the "locally ringed space foundations".

[Reid Barton]

I mean, ideally one's foundations should become irrelevant at some stage of the development, though I don't know whether this is going to be the case for everything on Sebastien's list.

[Reid Barton]

Well, I guess the main point is that eventually one will want to have the description in terms of atlases regardless of whether it is chosen as the definition or not.

[Kevin Buzzard]

This post is beginning to read like my Langlands brain dump from earlier this week. Can we get it into an issue somehow? That would rely on fleshing some of the ideas out

[Patrick Massot]

What extra structure do you have in mind? You can certainly do vector bundles, tangent bundles, metrics, symplectic structures, connections, curvature, exterior derivatives, almost complex structures very naturally from the ringed space viewpoint.

Do you mean: you can define manifolds as ringed space then derive existence of atlases and do everything naturally from there? If not then could you elaborate? Let's go for simpler stuff. What is your ringed definition of manifolds with boundary for instance?

[Johan Commelin]

I've never used manifolds with boundary, so I don't know exactly how functions on them are supposed to behave. But I'll take a stab:
A manifold with boundary of dimension $n$ is a locally ringed space $(X, \mathcal{O})$, such that: there exists an open set $U$ with the properties

• for every point $x \in U$ there is an open neighbourhood $U_x$ such that the induced LRS $(U_x, \mathcal{O}|_{U_x})$ is isomorphic (as LRS) to the standard open $n$-ball with the sheaf of $C^k$ functions on it;
• for every point $x \notin U$, there is an open neighbourhood $U_x$ such that the induced LRS $(U_x, \mathcal{O}|_{U_x})$ is isomorphic (as LRS) to the standard half $n$-ball with the sheaf of $C^k$ functions on it.

[Patrick Massot]

And what is the boundary then?

[Johan Commelin]

The interior consists of all points that have an open neighbourhood isomorphic to the standard open $n$-ball. The boundary is the complement of the interior.

[Johan Commelin]

Or do you mean that you want the boundary as LRS?

[Johan Commelin]

I guess you can take the induced reduced LRS structure on the closed subset.

[Patrick Massot]

I mean how do you recognize the interior using only the sheaf?

[Johan Commelin]

What I just said: it's the subspace of points that have a neighbourhood isomorphic to the standard open $n$-ball.

[Patrick Massot]

Hint: a function $f$ on the half $n$-ball is $C^k$ at $x$ is there is an open neighborhood $U$ of $x$ in $\mathbb{R}^n$ and a function from $U$ to $\mathbb{R}$ which restricts to $f$

[Patrick Massot]

What you define is everything

[Patrick Massot]

I think

[Patrick Massot]

Hmm, maybe you're saved by topology

[Johan Commelin]

Hmm, maybe you're saved by topology

Yup, that was my guess.

[Patrick Massot]

The sheaf is useless but the half ball is not homeomorphic to a full ball

[Patrick Massot]

That won't save you for manifolds with corners

[Johan Commelin]

What is a manifold with corners?

[Patrick Massot]

Locally modeled on a product of lines and closed half lines

[Patrick Massot]

Eg. $[0, 1]^2$

[Johan Commelin]

Locally modeled on a product of lines and closed half lines

This sounds suspiciously close to a LRS definition.

[Patrick Massot]

The corners are topologically impossible to distinguish from the codimension 1 strata of the boundary, and functions won't help you

[Patrick Massot]

This sounds suspiciously close to an atlas deifnition

[Neil Strickland]

I mean that:
1. Points of an open set U biject with homomorphisms C^∞(U,ℝ) → ℝ of ℝ-algebras
2. Vector bundles are the same as locally free modules over the structure sheaf. Fibres can be recovered by tensoring with characters as in 1.
3. Vector fields are ℝ-linear derivations, and individual tangent vectors are derivations with respect to a character as in 1.
4. The module of one-form fields is dual to the module of vector fields. The full de Rham complex is the exterior algebra of the one-form fields over the structure sheaf.
5. Connections on a vector bundle are actions of the Lie algebra of vector fields on the module of sections
And so on.

You can make all these definitions in a fairly straightforward and uniform way for any ℝ-algebra, and thus for sheaves of ℝ-algebras. You can prove properties for the sheaf of smooth functions on ℝⁿ, and deduce that they also hold for any ringed space that is locally isomorphic to that, which is the definition of a manifold.

[Johan Commelin]

The corners are topologically impossible to distinguish from the codimension 1 strata of the boundary, and functions won't help you

So we define it as a stratified LRS...

[Johan Commelin]

It seems to me that the atlas definition also needs extra data. The strata are part of the data, right?

[Patrick Massot]

No they are not

[Johan Commelin]

Hmm, ok

[Patrick Massot]

A diffeomorphism won't send a half plane to a quarter of plane

[Patrick Massot]

And of course none of this will bring you $(G, X)$-structures (for instance manifolds equipped with an atlas whose coordinate changes are in a given subgroup of $GL(n, \mathbb{R})$)

[Patrick Massot]

Neil, I'm sure you know this is all a joke. How can you hope to prove anything without reducing to the usual definitions? For instance, how to you equip $TM$ with a manifold structure and prove $TM \to M$ is a submersion?

[Patrick Massot]

Anyway, I should go and mark exams instead of feeding trolls

[Neil Strickland]

You certainly need to reduce things to properties of smooth functions on ℝⁿ. The only question is how to organise reduction to local properties. Standard books on differential geometry typically do not do this in a very thorough way that would be suitable for formalisation. If you try to fill in the details, you will end up recreating a lot of sheaf-theoretic stuff. In my opinion, it would be more efficient to build a decent library of sheaf theory, which will be needed for other reasons anyway, and use that explicitly.

[Andrew Ashworth]

@Kevin Buzzard I saw your MathOverflow post on manifolds did not have an answer, and coincidentally I was browsing through the archive of formal proof today and saw this: https://www.isa-afp.org/entries/Smooth_Manifolds.html. I have not had the time to read the paper so I do not know how much it overlaps with current efforts, but I thought I'd mention it.

[Andrew Ashworth]

Hah, in the paper the authors wrote (http://home.in.tum.de/~immler/documents/immler2018manifolds.pdf) they complain about simple type theory and ambiguous math textbooks.

[Kevin Buzzard]

Post a response!

[Johan Commelin]

@Sebastien Gouezel How far are we from defining a manifold structure on projective space?

1. Define projective space as a type. (Can be done for any field. Should later be connected to rational points of a scheme.)
2. Setup the coordinate charts
3. In the case that the base field is ℝ or ℂ, show that the coordinate changes belong to suitable groupoids.
4. Done?

[Sebastien Gouezel]

Yes, that's it. All of this should be pretty straightforward, at least if you use the naive version of projective space, i.e., quotient a finite dimensional vector space minus 0 by scalar multiplication. Even more straightforward would be to do it over the vector space fin (n+1) -> K, where one could use the standard n+1 affine charts.

[Johan Commelin]

Yes, that's what I was thinking of.

[Johan Commelin]

Are you working on things like open submanifolds, submersions, closed submanifolds defined by a regular value of a structomorphism, etc...?

[Johan Commelin]

Basically, I think I'm asking: what's the table of contents for your future PRs?

[Kenny Lau]

KP^n is a special case of Gr(n,k)

[Johan Commelin]

There are too many special cases here...

[Johan Commelin]

It's also a special case of a weighted projective space

[Kevin Buzzard]

it's also a special case of a projective variety

[Reid Barton]

Come on! This is about manifolds. It's clearly a special case of a symmetric space

[Johan Commelin]

Exactly... and my reflex is therefore to not make any examples at all... They are always to specific

[Johan Commelin]

But I think we need examples at some point.

[Kevin Buzzard]

https://github.com/leanprover-community/lean-perfectoid-spaces/tree/master/src/examples

[Kevin Buzzard]

I think Kenny at some point tried to make projective n-space as a scheme and failed---maybe it was even projective 1-space? We had to glue schemes, which meant we had to glue sheaves, and then we started down some rabbithole...

[Kenny Lau]

yeah I became lost in definition unfolding

[Sebastien Gouezel]

I am a little bit tired of definitions, so I think I will start proving a theorem, and see along the way which definitions I need. I would like to prove that an n-dimensional real manifold embeds into R^{2n+1}. This requires a partition of unity to embed it first in R^N for some large N, and then Sard theorem to decrease progressively the dimension by projecting along a typical direction and keeping an embedding. Given the amount of prerequisites, I expect this to be a long-term project :)

[Johan Commelin]

Is the 2n+1 "useful"? Of course it is nice to know. But isn't the N-version good enough for all practical purposes? I am really quite ignorant about these things...

[Johan Commelin]

Another nice long term goal (from my POV) would be Chow's theorem (closed analytic in P^n => algebraic). But maybe we should do some complex analysis first :lol:

[Sebastien Gouezel]

The 2n+1 is nice, although not optimal: one can do 2n, and even 2n-1 when n is not a power of two (but this is much more difficult). But what is really interesting is the proof, as it involves several tools that are really important.

[Sebastien Gouezel]

Just for the fun: do you know the smallest dimension N(n) such that any n-dimensional manifold can be immersed in R^N?

[Sebastien Gouezel]

It is N(n) = 2n-a(n), where a(n) is the number of ones in the base-2 expansion of n...

[Johan Commelin]

... lol, nice.

[Mario Carneiro]

do you know a 3D manifold that doesn't fit in 4D?

[Mario Carneiro]

oh, I guess that's covered by your more precise statement about 2n-a(n)

[Kevin Buzzard]

It is N(n) = 2n-a(n), where a(n) is the number of ones in the base-2 expansion of n...

I don't see how you can immerse S^1 in R :P

[Sebastien Gouezel]

I could edit my message to add the assumption n > 1 (I wish we could also do that for published papers :), but it is more honest to add it just now. So, standing assumption: n > 1. And I just checked the paper, there is also a compactness assumption by the way.

[David Michael Roberts]

A similar thing happens for proper holomorphic embedding of Stein manifolds (i.e. complex manifolds with sufficiently many nontrivial C-valued functions, more or less) into affine C^n. The case of open Riemann surfaces is a special case where we don't know if we can drop one more dimension in the target to match the uniform formula that works for all dimensions \geq 2. We know we can put them in C^3, the formula suggests C^2, though there are no counterexamples known.

[Johan Commelin]

I am a little bit tired of definitions, so I think I will start proving a theorem, and see along the way which definitions I need. I would like to prove that an n-dimensional real manifold embeds into R^{2n+1}. This requires a partition of unity to embed it first in R^N for some large N, and then Sard theorem to decrease progressively the dimension by projecting along a typical direction and keeping an embedding. Given the amount of prerequisites, I expect this to be a long-term project :)

@Sebastien Gouezel It just occurred to me that we are also getting towards a situation where we can state some form of Stokes' theorem. Does anyone know of a formalization of Stokes' theorem? The best I could find was an MSc project in Edinburgh that started working on it: http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=E6816A068653DFB139039B8F47C180AC?doi=10.1.1.64.7036&rep=rep1&type=pdf But I don't think they actually managed to get to Stokes' theorem.

[Sebastien Gouezel]

You have https://www.isa-afp.org/entries/Green.html for the 2-dimensional version, but I don't know of a general version. I think we are still pretty far in Lean: first one would need material of linear algebra on alternating forms, and then define differential forms and their integrals. Once one can state the theorem, I think proving it will not be hard (it just boils down to: use a partition of unity to reduce it to the half-space in R^d, and then integrate by parts in the vertical direction).

[Johan Commelin]

I agree that we aren't ready to do it right away. But it might be a nice goal to work towards

[Johan Commelin]

It seems that you are currently moving towards partition of unity

[Sebastien Gouezel]

It's definitely a nice middle-term goal, yes.