Reservoir

Towards the Sard-Smale theorem

In this repository, we work towards the proof of the Morse-Sard and Sard-Smale theorems.

Morse-Sard theorem. Let and be -manifolds of dimensions and , respectively and a map. If , the set of critical values of has measure zero in . Moreover, the set of regular values of f is residual and therefore dense. (There is a more general version, about the Hausdorff measure of the set of points where the differential has rank at most . Eventually, we also want to prove this one.)

The Sard-Smale theorem is a generalisation to infinite-dimensional Banach manifolds. Stating it requires a theory of Fredholm operators. See a separate file for detail and a roadmap towards that.

Applications of Sard's theorem.

• stronger version of Whitney's approximation theorem
• proving Brouwer's fixed point theorem: there is no retraction
  • needs smooth approximation during the proof; otherwise it just shows this for smooth retractions
• transversality theorem (the local part uses Sard's theorem)
  • already the theorem statement requires defining the strong and weak -topologies -> separate project
  • global part of the proof uses new ideas

Status

This project was initiated during Lean for the Curious Mathematician 2023, mentored by @fpvandoorn and continued thereafter. A fair amount of groundwork is done, but significant parts of that remain (and the "hard part" of the proof hasn't been started yet). I'm pausing this project for now (except possibly upstreaming the parts which are complete to mathlib) since my Lean time is limited; I intend to return to and complete this project if possible.

That said, help is very welcome! Feel free to make a PR filling in some sorry, or working towards the proof of the "hard" case.

Necessary steps/work plan

• pre-requisites

  • define locally Lipschitz maps; show C¹ maps are locally Lipschitz mostly PRed and merged

  • locally Lipschitz maps preserve null sets (done; mathlib mostly has this already)

  • nowhere dense and meagre sets: PRed and merged

  • -compact subsets, relation to -compact spaces and basic: PRed and merged

  • -compact measure zero sets are meagre: PRed

  • finite-dimensional manifolds are locally compact: PRed and merged

  • define measure zero subsets of a manifold: first version complete and PRed. Needs rework to a more conceptual approach:

    • define Lebesgue measure on a C¹ manifold (pull back Lebesgue measure on each chart, use a partition of unity)
    • re-define: a measure zero subset of a manifold is a null set w.r.t. one (or any) Lebesgue measure
    • show well-definedness: null sets are preserved by coordinate changes (see below)
    • show: has measure zero iff for each chart , the set is a null set
    • define the almost everywhere filter on a manifold, show it's a CountableIntersectionFilter
    • show the ae filter is induced from the charts
    • perhaps not all of these are truly required
• state Sard's theorem: formalised
• reduce to a local statement: essentially done (remaining sorries are busywork)
• "easy" case of Sard: if : essentially done
• "hard" case of Sard: : open, not started yet
  • show (in Hirsch's proof) has measure zero
  • inductive proof: base case is the previous bullet point
  • show has measure zero (similar argument)
  • remaining argument: induction proof, using a coordinate change and Fubini -> need to work out the details
• generalise to the Hausdorff dimension version
• follow-up/small extensions: handle manifolds with boundary; allow complex manifolds

File organisation

• MainTheorem.lean contains the statement of Sard's theorem and the reduction to the local case.

• ManifoldAux.lean contains miscellaneous results about smooth manifolds and their charts, used for reducing Sard's theorem to the local case.

• MeasureZero.lean contains the definition of measure zero subsets of a manifold (not reworked yet) and shows a -compact measure zero set is meagre.

• LocallyLipschitz.lean contains additional material on locally Lipschitz functions

• LocallyLipschitzMeasureZero.lean shows that locally Lipschitz functions preserve measure zero sets. Not PRed yet; a few sorries remain. This is essentially in mathlib (though phrased differently).

• Stuff.lean contains other results, which are superseded now.

• ObsoleteHelpers.lean contains results I didn't need; perhaps one or two lemmas are useful for mathlib.