Sard's theorem

Stream: maths

[Michael Rothgang]

During LftCM 2023 and continuing in the last two weeks, I've been working towards proving Sard's theorem in the general case. I'll put this aside for now to focus on finishing my PhD thesis. (I intend to return to it afterwards; probably not before March. I will respond to PR reviews etc., but not work on this more actively.)

If you are psyched about this, feel free to build on my work! The code's on github; I've made sure to document it well.

Progress so far. I've made a fair amount of headway, but it's by no means done yet. I'm still working through the prerequisites and easier parts. Overall, it's about 1150 lines of code (750 excluding docs and blank lines). As I'm quite new to Lean, I'm sure more golfing is possible :-)

More specifically, so far I have

• defined measure zero sets on a manifold (PRed to mathlib, will need rework before it can land)
• defined nowhere dense and meagre sets (PRed to mathlib, awaiting review)
• defined locally Lipschitz functions (basic properties shown, enough for Sard --- not PRed yet as I'd like to add more API)
• defined $\sigma$-compact subsets (mathlib had sigma-compact spaces already)
• shown: $\sigma$-compact measure zero sets are meagre
• shown: locally Lipschitz functions preserve measure zero sets
• most of a proof of the local version of Sard if $\dim M < \dim N$. (This is the "easy" case, as then the image of $f$ has measure zero. No need to analyze the critical set further.)
• stated Sard's theorem, in local and global versions

Notably missing are

• remaining sorries for the local proof
• reducing the global version to the local version of Sard
• proving the "hard case" $\dim M \geq \dim N$: this involves decomposing the critical set into several pieces, and showing each piece has measure zero using double induction over the dimension: this will be a significant amount of work.

[Yury G. Kudryashov]

Am I right that there is a version of Sard's theorem with an estimate on the Hausdorff dimension instead of measure zero?

[Yury G. Kudryashov]

BTW, for the "easy" part $\dim M < \dim N$, docs#ContDiffOn.dimH_image_le gives a proof for normed spaces. I'm not sure if I can easily get rid of the convexity assumption.

[Sebastien Gouezel]

Yes, the optimal version of Sard theorem is phrased in terms of Hausdorff dimension. See https://en.wikipedia.org/wiki/Sard%27s_theorem. The interesting part of the proof has nothing to do with differential geometry, it is for maps between finite-dimensional real vector spaces.

[Sebastien Gouezel]

(Note that apparently wikipedia's statement is wrong, see https://math.stackexchange.com/questions/416607/show-that-fc-has-hausdorff-dimension-at-most-zero/446049#446049 -- it would be good to formalize the correct version and fix wikipedia accordingly :-)

[Yury G. Kudryashov]

I read Sard's paper last week. In case of a manifold with boundary, he assumes that the function can be extended to an open set without loss of smoothness.

[Yury G. Kudryashov]

Is it true for our definition?

[Yury G. Kudryashov]

Without this, we would need a version of the inverse function theorem for functions defined on a closed half-space.

[Sebastien Gouezel]

Yes, a function which is smooth on the closed half-space can be extended to a smooth function on the whole space. It's a special case of Whitney's extension theorem https://en.wikipedia.org/wiki/Whitney_extension_theorem

[Sebastien Gouezel]

But I think it would make sense to first prove Sard in the boudaryless case, and then revisit if/when needed the case with boundary.

[Michael Rothgang]

The above is probably conceptually more correct --- but there's a "simpler" argument for Sard with boundary: show that the boundary of a manifold has measure zero. This follows from the easy case of Sard once the boundary is shown to be a submanifold.

Does our definition of boundary imply it's a submanifold (perhaps with boundary and corners)? I'm not sure if does, but conceptually it should.

[Michael Rothgang]

I'm putting simple in quotes: formalising this probably requires that interior and boundary are independent of the chosen chart. This is true, but AFAIK requires e.g. homology of spheres. (As I understand it, this is still a few months away - be it with singular homology or de Rham cohomology.)

[Yury G. Kudryashov]

Sard's theorem has a version for maps from R^m to R^n with m>n and the image of the set of points of rank r < n.

[Yury G. Kudryashov]

I went through the first several pages of the paper in branch#YK-sard. I'm working on another project this week but I'm going to revisit it next week.

[Michael Rothgang]

Yury G. Kudryashov said:

Sard's theorem has a version for maps from R^m to R^n with m>n and the image of the set of points of rank r < n.

Exactly, that's the "easy" version of Sard we'd need to show the boundary has measure zero.

[Yury G. Kudryashov]

Note: with m > n, not with m < n.

[Yury G. Kudryashov]

This is not the easy version. That's where we may need higher differentiability.

[Yury G. Kudryashov]

And if m > n + 1, then the easy version won't help with the boundary.

[Michael Rothgang]

Michael Rothgang said:

I'm putting simple in quotes: formalising this probably requires that interior and boundary are independent of the chosen chart. This is true, but AFAIK requires e.g. homology of spheres. (As I understand it, this is still a few months away - be it with singular homology or de Rham cohomology.)

Actually, there's another way: e.g. Roig-Domínguez have a definition of Banach manifolds with boundary and corners - and show that diffeomorphisms (of class at least C¹) preserve interior and boundary. Their definition of boundary is more specialised that mathlib's, though.
See https://arxiv.org/pdf/1910.14580.pdf, Theorem 4.12 - the textbook is paywalled (but my uni has access to it).

Summing up: I'd wait until Banach manifolds with boundary come up somewhere.

[Michael Rothgang]

Yury G. Kudryashov said:

And if m > n + 1, then the easy version won't help with the boundary.

I thought about a different argument: The boundary $\partial M$ is a codimension one submanifold of $\partial M$, hence has measure zero in $M$.
As $f$ is locally Lipschitz, the image $f(\partial M)$ also has measure zero.