Looking for Differential Geometry Project

Stream: new members

[Jack McCarthy]

Hello Lean community!

My name is Jack M. I'm a graduate student in mathematics at Stony Brook University in New York. My main interests lie in differential geometry/topology, mathematical physics, and of course formalization!

I am looking for a good introductory project to help contribute to Mathlib, preferably something in smooth manifold theory. For example, I saw that there was a recent PR implementing smooth immersions #28793, and I'd like to work on some of the suggestions made in that PR such as defining smooth embeddings and smooth submanifolds—although I'm open to helping on any other open projects as well!

Can anybody give me advice on the best way to go about something like this? The contributer guide advises to "discuss your contribution before and while you are working on it." Is there a particular thread where I should go about this?

Edit: if you are based around New York, I am very open to collaborating in-person

Thanks,
Jack

[Kevin Buzzard]

Here is a fine place to ask (although if you edited the title of your post to "Looking for differential geometry project" you might get more of the relevant eyes on it). I am not at all up to date with what's going on in differential geometry but I am wary of the fact that "make a definition" projects are often not good for beginners, because design decisions are a subtle part of formalization; beginners are usually better off doing "prove a theorem" projects.

Something I need in my own work is Jacobian of a compact Riemann surface. Here is a naive question: can we construct the map $H_1(X,\Z)\to H^0(X,\Omega^1)^*$ for a compact Riemann surface and prove that the image is a lattice? Here's another one: can we prove that any nonconstant morphism between compact connected Riemann surfaces has a degree? And a harder one: can we prove that any compact Riemann surface is algebraisable? I only mention these because they're relevant to things I want to do, I have no idea how accessible they are right now.

[Rémy Degenne]

@Michael Rothgang can probably advise on good projects

[Yan Yablonovskiy 🇺🇦]

Me and @David Wiygul are wanting to get Fredholm operators in, maybe that might interest you. Have a look at #new members > elliptic PDEs @ 💬

[Notification Bot]

This topic was moved here from #new members > Introduction and Looking for Project by Jack McCarthy.

[Jack McCarthy]

@Kevin Buzzard Those are very nice problems you raised about Riemann surfaces, but these seem a little bit difficult for a first project. I am also not very deep into the homological algebra / complex analysis side of topology, I'm moreso interested in dynamics and analysis.

For instance, I noticed that Matlib overview currently does not contain the generalized Stokes Theorem, or a definition of the (geometric) Laplacian, or any major results about Riemannian metrics, flows, Morse theory, etc. -- and I wonder if working towards one of these could be a good place to start.

Out of curiosity, what are the project you're currently trying to do which require these results about Riemann surfaces?

[Kevin Buzzard]

I'm trying to prove Fermat's Last Theorem.

[Jack McCarthy]

That is epic. I have a few friends who have done work on Riemann surfaces and are interested in formalization. I will ask them to look at these problems.

[Julian Berman]

Edit: if you are based around New York, I am very open to collaborating in-person

(You are quite welcome in #Geographic locality > New York City, USA and to meet up if you're ever towards the city, especially if you don't expect us -- or at least me -- to know the first thing about differential geometry!)

[Jack McCarthy]

@Julian Berman I would love to meet up in the city! I noticed that there was a Google Groups page made to host calendar events. Do you know if this group still active ? (I do not have permission to access it) Or is it best to just look in the Zulip channel for meeting times?

[Julian Berman]

When we meet up (which is usually every week, though this week I'm personally away) we always put it in Zulip, but yeah we have the group as well, if you send a membership request I'll add you.

[Michael Rothgang]

Welcome; I'm very happy to hear you're interested in differential geometry! I'm happy to suggest new project ideas. I'm on my phone now, but will get back to you very soon

[Jack McCarthy]

@Michael Rothgang Yes please I'd love project ideas! For some background, I have spent the last year carefully working through all of the exercises in Lee's "Intro to Smooth Manifolds" textbook, which is a standard diff-geo reference used in other PRs to mathlib. It includes such results as the complete classification of 1-manifolds, existence/uniqueness of short-times solutions to 1st-order quasi-linear PDEs, and the Hairy Ball Theorem, all of which I think would be very nice to formalize.

[Kevin Buzzard]

Complete classification of 1-manifolds is something that Steve Sivek at my uni is interested in seeing formalised. Surely hairy ball has been done by now?

[Bennett Chow]

Hi @Jack McCarthy , this past week or two, Jack Lee and I were working together on writing a detailed, Lean-friendly, LaTex file on the definition of tangent space using derivations and proving that the coordinate tangent bases $\{ \partial/\partial x^i\}$ form a basis of the tangent space $T_xM$ at each point $x$ in the coordinate chart. I thought it would be just a couple of pages, but it ended up being over 20 pages. I would like to formalize this into Lean as an alternate (more canonical IMHO) definition of tangent space. Derivation is already in mathlib4, but it is not yet connected to the model space stanard Lean definition of tangent space. More generally, we would like to start a discussion of the definition of manifold in Lean. I'm sure there are good reasons to add "with corners" as it is, but for someone working in Ricci flow, a far more important generalization for us is smooth orbifold with isolated singularities. These structures are actually smooth at the "singularities" in the sense that all geometric objects and morphisms are smooth by passing to the local lifts and considering them equivariantly. We also would like work on developing tensor calculus, and my Ph.D. student @Yuan Liao (with the help of @Michael Rothgang ) is one of the people working on this.

[Bennett Chow]

@Jack McCarthy , It would be incredible to get Stokes' theorem in mathlib4. @Yury G. Kudryashov is the expert on many things, but he has also specifically coded Stokes' theorem in Euclidean space and it would be amazing if we could have this generalized to compact manifolds with or without boundary. Some consequences, such as the divergence theorem and integration by parts would be foundational for geometric analysis and Ricci flow. In particular, the weak maximum principle and integration by parts are the two most fundamental analytic tools for Ricci flow.

[Bennett Chow]

@Jack McCarthy , It would also be incredible to get the Laplacian on a Riemannian manifold defined. @Patrick Massot and @Michael Rothgang are developing the Levi-Civita connection. It would be great to develop the covariant derivative of tensors (after tensors are developed). In addition to the Laplacian acting on scalar-valued functions, it would be great to develop the rough Laplacian acting on tensors (trace of the second covariant derivative). After the Riemann, Ricci and scalar curvature tensors/function are developed (which I imagine would not be so hard after Levi-Civita connection), then one would be able to derive the commutator formulas for covariant differentiation acting on tensors. I think there would be a lot of interest in that.

[Bennett Chow]

@Jack McCarthy , for Riemannian surfaces (not Riemann surfaces), it would be great to formalize 2-dimensional Ricci flow. There is a theorem of Hamilton where he proves convergence to constant curvature for the Ricci flow on surfaces (see the reference in https://projecteuclid.org/journals/journal-of-differential-geometry/volume-33/issue-2/The-Ricci-flow-on-the-2-sphere/10.4310/jdg/1214446319.pdf ). This was generalized to 2-dimensional orbifolds with isolated singularities by his student Lang-Fang Wu (https://onlinelibrary.wiley.com/doi/abs/10.1002/cpa.3160440302 ), where the convergence is to a shrinking Ricci soliton. Note, Seifert fibered spaces be considered as circle (orbi)bundles over 2-dimensional orbifolds with isolated singularities. Extending the Hamilton--Perelman work, Kleiner and Lott (https://www.numdam.org/book-part/AST_2014__365__101_0/ ) gave a Ricci flow proof of the orbifold geometization conjecture/theorem. In 4D, since spherical space forms $S^3/\Gamma$ can pinch, one is forced into the orbifold category by any conceivable Ricci flow with surgery. Also, the Eguchi--Hanson Ricci flat hyperk\"ahler ALE can form as a singularity model by the work of Appleton https://arxiv.org/abs/1903.09936 (perhaps all Kronheimer spaces can too?). So there is another way the orbifold category comes up in 4D, even starting Ricci flow from a smooth closed 4-manifold.

[Bennett Chow]

@Jack McCarthy , A further formula that would be nice to formulate in Lean is the formula for Hamilton's Ricci flow surface entropy (see https://projecteuclid.org/journals/journal-of-differential-geometry/volume-33/issue-2/On-the-entropy-estimate-for-the-Ricci-flow-on-compact/10.4310/jdg/1214446332.full ). This combines both Riemannian surfaces and integration by parts (via Stokes' theorem) in a simple, but conceptually important setting. This formula is the first place where an entropy monotonicity was directly connected to shrinking Ricci solitons (and was quoted by https://arxiv.org/abs/math/0211159 ). Note, the original proof of the convergence used an entropy-energy comparison (https://projecteuclid.org/journals/journal-of-differential-geometry/volume-33/issue-2/The-Ricci-flow-on-the-2-sphere/10.4310/jdg/1214446319.pdf ), where the energy is the zeta function regularized definition of the determinant of the Laplacian as was studied, among others, by Osgood, Phillips, and Sarnak (https://www.sciencedirect.com/science/article/pii/0022123688900705 ), and used an energy lower bound of Onofri. This 2D (relative) energy actually can be interpreted as a Bott--Chern secondary characteristic class, and in that sense, in a tangential way related to Donaldson's work on (Anti-Self-Dual) Hermitian--Yang--Mills on algebraic surfaces (https://londmathsoc.onlinelibrary.wiley.com/doi/abs/10.1112/plms/s3-50.1.1 ). The determinant line bundles aspect was discussed by Donaldson in his work on Hermitian--Yang--Mills over algebraic manifolds, but the key force in that paper was actually a theorem of Mehta and Ramanathan in algebraic geometry where semi-stable bundles restricted to hyperplane sections are semi-stable, allowing for an induction argument on dimension (https://projecteuclid.org/journals/duke-mathematical-journal/volume-54/issue-1/Infinite-determinants-stable-bundles-and-curvature/10.1215/S0012-7094-87-05414-7.short ). In any case, the intergration by parts formula is one way to bypass the energy-entropy connection since in the 2D bad orbifold case, the energy is not bounded from below.

[Jack McCarthy]

@Bennett Chow I absolutely agree with the roadmap you set forth for formalization in differential geometry. Beginning with the definition of a tangent space is an obviously necessary step. And simultaneously developing the cases for manifolds with boundary/corners would be prudent for many applications. I am less confident on the theory of orbifolds, as I am most confortable with the case of a simply connected manifold M quotient by a finite group Γ.

Stokes Theorems and the Laplacian operator I agree are good goals to demonstrate progress in manifold theory. For instance, I have done some work in harmonic analysis, so I would be interested in proving some geometric results about the Laplace-Beltrami operator and it's eigenvalues/eigenfunctions. Some results about Ricci curvature and the Lie derivative will also likely be necessary before the work on Ricci flow can begin in earnest. As you suggest, working on the case of 2-dimensional Riemannian surfaces and Hamilton's Ricci Flow Surface Entropy could be a good place to start. I am also very interested in the topic of curvature and energy estimates/bounds that you brought up, especially in the pseudo-Riemannian setting as these arise in the work of e.g. Choquet-Bruhat, Mondal, Anderson for proving the existence/uniqueness of solutions to the Einstein Vacuum Equations, which would be a significant result for mathematical physics if it could be formalized.

[Yury G. Kudryashov]

About Stokes thm: I'm working on getting basic facts about differential forms into Mathlib. Once this is done, transferring the theorem itself should be easy.

[Jack McCarthy]

@Yury G. Kudryashov That's great to hear! I'd love to help with the differential forms project. Do you know if there are any PRs with sorrys that need filling? For example, right now I am working on filling a few remaining sorrys in PR #26743 on the Product Rule for Lie Brackets.

[Yury G. Kudryashov]

The next goal is to introduce a "continuous alternating maps" operation on vector bundles, copying most of the API from the file about continuous linear maps. Also, there may be some material in this file about it. It's possible that this file (with dependencies) is ready to be upstreamed as is, or it may be outdated.

[Yury G. Kudryashov]

If you have time to compare it to the file about continuous linear maps and update it on its way to Mathlib, that would be great.

[Michael Rothgang]

@Jack McCarthy Thanks for helping out with #26743 --- but please talk to me when doing so, to avoid wasted work! I have further progress on this in #26221. (In fact, it is "almost done", in the sense that I only need to generalise one lemma from mfderivWithin of one set to one on a larger set. Help with that last fiddling is welcome.)

[Michael Rothgang]

(I'll write a proper response with my project suggestions within the next hour.)

[Jack McCarthy]

@Michael Rothgang Sorry about that, I meant to talk to you but wasn't sure what was the best way to reach out. I will look into #26221. And thank you in advance for project suggestions!

[Michael Rothgang]

You can always write me a direct message on zulip. (In fact, let me also point you towards the current state of #26743 in a moment, via DM.)

[Jack McCarthy]

Great, thanks!

[Michael Rothgang]

Thanks for your patience, and welcome again to mathlib! It's great to hear that you have strong background in differential geometry. This area is a bit tricky in Lean, so you knowing the mathematics well is very useful. What's your Lean background so far? Have you never written any Lean code yourself, taken a course in it, worked through mathematics in Lean, done a project already? (All of these are fine, but my suggestions would change accordingly.)

[Michael Rothgang]

Differential geometry in mathlib is somewhat under construction right now: many useful results are in an external project, waiting for review or "almost done". Some examples:

• differential forms: @Yury G. Kudryashov and @Sam Lindauer have worked on them and made lots of progress, but some works remains to be done. The current focus is getting the results so far merged into mathlib. I'm sure help with the remaining sorries is welcome (but you'd have to ask Yury for details).

• submanifolds: I'm working on those. Most of the work is done, and this is mostly waiting for review.
  I'm defining immersions first, then smooth embeddings, and embedded/immersions submanifolds in terms of those. The first part (defining smooth immersions, in the correct way for mathlib) should be merged very soon, hopefully this week. At this point, I'm not sure if outside help is useful: this will change in the future (once some basics are in place), but probably not for a month or two.

• I am advising a student who will work on submersions and the regular value theorem --- so working on that would be doubling effort. (If you want to use those, I'm happy to state the key results for you.)

• connections, in particular the Levi-Civita connection. Patrick Massot and I have proven the uniqueness (and most of existence) of the Levi-Civita connection. We're working on the last pieces of the proof (and on getting this into mathlib).

[Michael Rothgang]

Building on all of these is possible, but involves some additional logistics (preparing a branch with the right results, and probably a bunch of sorries).

[Michael Rothgang]

That said, there are many areas where your help would be most welcome:

• We have the implicit and inverse function theorem on normed spaces, but not for manifolds. There's an old PR which proves the inverse function theorem for manifolds, which is very close to done. (I'd need a focused day, perhaps less, to complete it.) Help with that is welcome; I'm happy to provide instructions.
• We don't have orientations on manifolds yet. @Rida Hamadani worked on them, and it's again "almost done", but help completing this work is appreciated. Defining orientations on a manifolds, orientable manifolds and the product orientation would all be very useful (and necessary for Stokes' theorem).
• You may also need the collar neighbourhood theorem for Stokes' theorem. To state this in Lean, you need a notation of "manifolds whose boundary is a closed smooth manifold". I have this definition (and a statement) in an open PR, and could provide guidance on the proof.
• You could work on gluing of manifolds: gluing two manifolds e.g. along a common collar. The first step would be to define this on the topological level, i.e. defining attaching maps/pushouts in the category of topological spaces. (We know abstractly that they exist, but giving a concrete description would be helpful. There have been previous attempts I can link you to.)
• We also don't have quotients of manifolds either: if $M$ is a smooth manifold and $G$ is a discrete group acting properly on $M$, the quotient is a smooth manifold. (This way, you could exhibit e.g. real projective space as a smooth manifold.)

[Michael Rothgang]

• The classification of (e.g. connected) 1-manifolds is also missing from mathlib. There is again previous work, that did not complete the project (and didn't end up in mathlib).

[Michael Rothgang]

Commenting on the particular ideas proposed in this thread:

• Stokes' theorem would be great, but we need some prerequisites first: differential forms, orientations and the induced orientation on the boundary.
• mathlib doesn't have orbifolds yet. @Ben Eltschig has been working on these (via diffeological spaces). I'm not sure what the precise status is; finding a suitable reviewer in mathlib has been challenging.
• We don't have the hairy ball theorem yet, because the story with singular homology is complex: Sean Brendas Murphy defined it in Lean 3 (and proved the Eilenberg-Steenrod axioms, computed the homology of spheres and deduced Brouwer's fixed point theorem). The homology algebra part of that project was not ready for mathlib, though and has been completely rewritten since then. We now have singular homology in mathlib, but somebody needs to go and re-do the proofs of the E-S axioms. (This would be another sorely needed project, but more on the topology side.)
• Defining the Laplacian on a Riemannian manifold should certainly be doable. (The logistics on top of the Levi-Civita branch might be a little complex, but should be manageable.)

[Michael Rothgang]

I'm not sure I follow the motivation for re-doing tangent spaces here. Mathlib certainly has them (docs#TangentSpace), and it also has the canonical basis on them, abstractly.
(For instance, let us describe the principal part of a vector field $X$ on $M$. A chart is a local trivialisation of the tangent bundle, which induces a local frame on $TM$. The principal part of $X$ are the coefficients of $X$ (considered as a section of $TM$) in that local frame. We have local frames in mathlib, and the coefficients (...) are almost ready to be merged.)

If your blueprint is already 20 pages, that sounds like a significant amount of work to formalise... the gains of which are not clear to me.

[Michael Rothgang]

Phew, that was a long answer. I hope this is helpful. Don't hesitate to ask if something is unclear.

[Michael Rothgang]

I'm happy to mentor you for most of the projects I proposed above; feel free to get in touch!

[Michael Rothgang]

Another idea that was mentioned is Sard's theorem: @Yury G. Kudryashov and I started formalising it, but it's currently on hold as we're both busy with too many other projects. I'd certainly like to revive it at some point (and am happy to do that together).

[Oliver Nash]

A potentially fun project would be to prove that the metric docs#UpperHalfPlane.dist_eq arises from the Riemannian metric $(dx^2 + dy^2)/y^2$. See #mathlib4 > Hyperbolic space

This is likely to contain some quite fiddly stuff but I think it is likely to contain some nice elementary geometry and basic API development as you go.

[Bennett Chow]

Great to hear that @Yury G. Kudryashov and @Sam Lindauer have made good progress on differential forms, and Stokes' theorem. After Levi-Civita connection by @Patrick Massot and @Michael Rothgang are done, besides the curvature tensors, it will be great to get the divergence theorem for a Riemannian manifold with or without boundary. Then we can do integration by parts. A first intermediate goal could be Perelman's $\mathcal{W}$-entropy monotonicity formula. Perhaps simpler would be my entropy formula for Hamilton's surface entropy $\int R \ln R$. Both formulas connect an entropy-type monotonicity to shrinking gradient Ricci solitons, but the latter (although it has limited use since it only holds in 2D and is far surpassed by Perelman's general all dimensions formula) might be easier to code in Lean.
Regarding the Laplacian, it would also be great to get the rough Laplacian on tensors. In Ricci flow, we don't really use the Hodge Laplacian acting on forms too much, since most quantities are tensors, and not forms.
Great that @Ben Eltschig is thinking about orbifolds. Note, realistically, if Ricci flow is to have applications to smooth manifold topology in higher dimensions, it's going to be in 4D first. Here, Bamler's theory indicates the smooth orbifolds with isolated singularities is the correct category, even if one starts with smooth 4-manifolds (they arise by pinching spherical space forms). But key will be to able to do geometric analysis on these orbifolds, in particular, tensor calculus and extend Stokes' theorem, divergence theorem, integration by parts to this category.
For the tangent spaces blueprint, we may not use it, but it was a good exercise for us.
The submanifold theory is also important to Ricci flow, especially hypersurfaces. It would good e.g. to get second fundamental form and the mean curvature function/vector. I guess after that one of the first things to prove are the Gauss and Codazzi equations.

[Jack McCarthy]

Michael Rothgang said:

What's your Lean background so far? Have you never written any Lean code yourself, taken a course in it, worked through mathematics in Lean, done a project already?

I've worked through mathematics in Lean and the exercises from the "Lean for the Curious Mathematician" colloquium. I've not done my own project yet, but I have contributed to a few repos like the ongoing Brownian Motion project.

Regarding the project you discuss, the one that interests me the most is orientations on manifolds and the hairy ball theorem. I also do not think you necessarily need singular homology to do the Hairy Ball Theorem, there is a much more elementary proof outlined in Lee, Smooth Manifolds, pg. 435 which only uses only Stokes Theorem.

I'm also quite interested in the Sard's Theorem project, since this would unlock many other useful theorems like the Transversality of Smooth Families. I will ask Yury for more details when I have time to work on it. Right now I am trying to help him with the DeRham Cohomology project.

[Jack McCarthy]

Oliver Nash said:

A potentially fun project would be to prove that the metric docs#UpperHalfPlane.dist_eq arises from the Riemannian metric $(dx^2 + dy^2)/y^2$.

This is great idea! Also, if we have the notion of the induced Riemannian metric (is this in Mathlib yet?) it would be nice to show how the metric $(dx^2 + dy^2)/y^2$ is related to the pushforward of the induced metric on the hyperboloid under stereographic projection.

[Yury G. Kudryashov]

I've resumed work on Sard's Theorem last week. So far, I'm doing some simple lemmas. I'll try to figure out what's the current status of the project this weekend.

[Michael Rothgang]

Sounds you know a fair bit of Lean already, great!

[Michael Rothgang]

So for the next steps, I gather you're working on the Lie bracket sorry and helping out with differential forms? Both sounds very nice and useful. (Or would you also like to look into orientations? If so, feel free to get in touch and I can point you at previous work and what would need to change.)

[Yury G. Kudryashov]

BTW, some day we should generalize the manifold structure on bundles from vector bundles over manifolds to topological bundles with both the base and the fiber being manifolds.

[Yury G. Kudryashov]

E.g., I would prefer to have connections defined in these settings.

[Sébastien Gouëzel]

I'm not sure I understand the subtlety here. Don't we already have this is you require that the base is a C^1 manifold, but the vector bundle is a C^0 manifold? But I'm not sure I see what a connection is in this setting, could you elaborate?

[Yury G. Kudryashov]

Quite possibly, I've missed a refactor.

[Yury G. Kudryashov]

Last time I looked at this folder, the fiber was assumed to be a vector space.

[Yury G. Kudryashov]

E.g., https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Manifold/VectorBundle/Basic.html#Bundle.TotalSpace.isManifold

[Sébastien Gouëzel]

Ah, sorry, the point is you want a connection on a manifold bundle, not a vector bundle, right? These are different beasts, as far as I understand, i.e., there are additional properties related to linearity that connections on vector bundles should satisfy.

[Yury G. Kudryashov]

Linearity, or something else?

[Yury G. Kudryashov]

If it's just (some kind of) the linearity, then we can have connections on manifold bundles and linear connections on vector bundles that extend connections on manifold bundles.

[Yury G. Kudryashov]

Note: it's rather late here, so the probability of me writing nonsense is higher than usual.

[Michael Rothgang]

I absolutely agree mathlib should have a nice theory of smooth fiber bundles! But AFAIK it doesn't have that yet. (I'm also interested in making that happen, so we can finally get the global parts of sphere eversion into mathlib. But one step at a time, I'll try to "finish" submanifolds and the Levi-Civita connection first.)

[Yury G. Kudryashov]

I think that generalizing most of Manifold/VectorBundle to fiber bundles may be a nice project to learn about the way manifolds are done in Mathlib.

[Jack McCarthy]

Yury G. Kudryashov said:

I think that generalizing most of Manifold/VectorBundle to fiber bundles may be a nice project to learn about the way manifolds are done in Mathlib.

This is a good idea as well. Highly adjacent to the work on differential forms / tensor fields as well. It will also be useful to define categorical functors on vector bundles. For example, prove that the covector bundle is the dual of the vector bundle; That we can combine vector/covector fields together with the wedge product, tensor product, symmetric product, interior multiplication, etc. to form higher order tensor fields.

Edit: What about the code in Topology/FiberBundle? That it is not a smooth manifold?

[Michael Rothgang]

Everything Topology/FiberBundle is about topological spaces; no smooth structure.

[Michael Rothgang]

I'm not sure how approachable "generalise Manifold/VectorBundle to smooth fiber bundles" is as a (close to) first project. I won't be able to help with this much this year (too many other commitments); this will improve in January/February.

[Michael Rothgang]

Getting e.g. oriented manifolds into a mergeable state would be more useful for mathlib, in the short term.

[Nick_adfor]

Oh, I never think that there's Differential Geometry Project. I was reading Milnor's Topology from Differential Viewpoint and Morse Theory these days. I may want to check some work in Lean.

[Yury G. Kudryashov]

https://github.com/urkud/SardMoreira/ is mostly done (main theorem is sorry-free, code needs some cleanup on its way to Mathlib).

[Yury G. Kudryashov]

Help with upstreaming the proof to Mathlib is very welcome.

[Michael Rothgang]

I'm very happy to help. My next three weeks are very busy, but it will slow down after that.

[Pietro Monticone]

Happy to help as well in the next few days.

[Yury G. Kudryashov]

I think it makes sense to get some lemmas from https://github.com/urkud/SardMoreira/blob/main/SardMoreira/ContDiff.lean into Mathlib first.

[Yury G. Kudryashov]

I'm not ready to coordinate the upstreaming effort until tomorrow. By tomorrow, I'll try to create a roadmap for upstreaming stuff.

[Yury G. Kudryashov]

Also, it would be nice to get rid of ContDiffMoreiraOn, or redefine it as ContDiffMoreiraAt all points of a set (thus get rid of U).

[Yury G. Kudryashov]

We never actually need U, but some lemmas need adjustment.

[Ruben Van de Velde]

Picked up two lemmas at #32977

[Sébastien Gouëzel]

I have a question: if I read correctly the statement you have posted, it's for full derivatives, so it won't apply to functions on domains, for instance functions in half-planes, right? Won't that create difficulties when trying to get a manifold version of Sard?

[Yury G. Kudryashov]

Yes, it's for full derivatives. I see 3 ways to make it work on manifolds:

• come up with a reasonable version of the inverse function theorem; I don't know any;
• assume for now that the manifold is boundaryless;
• formalize Whitney extension theorem.

[Yury G. Kudryashov]

The proof heavily relies on the implicit function theorem, and I don't know how to make it work without it.

[Yury G. Kudryashov]

Let's continue the Sard-Moreira discussion on #maths > Moreira-2001 (generalization of Sard's theorem)

[Nick_adfor]

Generalization to Hausdoff measure makes me hard to understand:( I have to go back to Milnor's old version on Lebesgue measure...

[Yury G. Kudryashov]

Hausdorff measures were there since Sard's 1942 paper.

We prove the following result: If $m\le n$, the set of critical values of
the map (1.1) is of m-dimensional measure2 zero without further hy-
pothesis on q; if $m>n$, the set of critical values of the map (1.1) is of
n-dimensional measure zero providing that $q\ge m — n + 1$

[Nick_adfor]

In Milnor, it uses a line like

$f(C) = f(C \setminus C_1) \cup f(C_1 \setminus C_2) \cup f(C_2 \setminus C_3) \cup \cdots \cup f(C_{k-1} \setminus C_k) \cup f(C_k)$

and Fubini Theorem on Lebesgue measure.