Moreira's version of Sard's Theorem

This project formalizes Moreira's version of Sard's Theorem. Currently, the main theorem is formalized, but some corollaries aren't.

Autogenerated docs can be found here.

Upstreaming to Mathlib

The ultimate goal is to upstream the main theorem. See ToMathlib for material that is ready to be upstreamed. Small lemmas from other files are good to go too.

If you're going to PR a larger feature that is outside of ToMathlib, then please talk to me (@urkud) first. I want to do some changes to the code before upstreaming, see below for details on some planned changes.

When you open a Mathlib PR with some material from this repo, please also open a PR to this repo that moves this material to SardMoreira/ToMathlib/PRNNNN.lean, so that we can easily see what was already upstreamed.

Planned changes

I was writing this project aiming to get to the result, while maintaining a reasonable quality of code. However, I almost never cleaned up parts of the code that I found to be suboptimal after they were written.

ContDiffMoreiraHolderOn

I think that we should get rid of this predicate. It attaches an open neighborhood to the interesting set for no good reason.

We may want to have a predicate saying that a function is ContDiffMoreiraHolderAt at every point of a set. What would be a good name?

A PR to this repo deleting ContDiffMoreiraHolderOn would be very welcome. AFAICT, the only slighlty challenging part is rewriting a lemma in ImplicitFunction.

Implicit function theorem

In ImplicitFunction, I define implicitFunctionDataOfComplementedKerRange as a constructor for ImplicitFunctionData. This version of the implicit function theorem was used, with slight variations, in all proofs of Sard's theorem, starting with the original Sard's paper.

This constructor forces a user to use classical choice to find a projection onto the range of the derivative. While this may be a good solution short term, in the future we may want to provide this projection explicitly, so that it satisfies some additional properties.

I think that the right design is to define a structure ImplicitFunctionDataNonSurj that will include a projection onto the range, then define a projection to ImplicitFunctionData.

Another option is to refactor ImplicitFunctionData to decouple the codomain and the space that is the range of the derivative. The challenging part here is to give the definition so that we can optionally make these spaces defeq, if we want.

I haven't seen the version of the implicit function theorem in chartImplicitData elsewhere, so I would consider it an implementation detail for now, unless someone comes up with another usage example, then we can think about a better API (e.g., not forcing ContDiffMoreiraHolderAt).

Vitali families and differentiation of outer measures wrt measures

One of the tricks I use in this repo to deal with the fact that we can't easily take the pullback of a measure is to let μ by an outer measure whenever we only estimate it from above.

I think that it would be useful to refactor more of the code about Vitali families and differentiation of measures to use this approach.

Given that we deal with "allmost all points" and a zero-measure set of points differently anyway, I'm not sure that we should have the ClosedBallCoveringMeasure typeclass, though we may want to have it just for zero-measure sets, just to make theorems about Besicovitch.vitaliFamily available in the context of uniformly doubling measures. I think that this should be discussed on Zulip before upstreaming the relevant code.

LinearMap.ker/LinearMap.range for ContinuousLinearMaps

While these definitions work both for LinearMaps and ContinuousLinearMaps, there is virtually no API for kernels and ranges of ContinuousLinearMaps.

I'm not sure what's the right way to fix this: add API, redefine range and ker, something else?

Simplifications in {x // x ∈ LinearMap.range f}

Since coercions of SetLike objects to Type* gets unfolded, in some cases Lean simplifies inside {x // x ∈ LineraMap.ker f}, then fails to apply lemmas that require x : LinearMap.ker f.

That's another topic worth discussing on Zulip.

Measure in a ball vs on a radial segment

In order to prove an o-small estimate on f y - f x near a Lebesgue density point of the set {x | fderiv f x = 0}, I need to show that a set of a small measure in a ball meets most (in terms of measure) of the radial segments on a set of small measure.

Currently, the proof uses compactness arguments here and there, but one can show that the constants involved in the statement depend on the dimension of the domain only, not on the norm or the codomain.

While this is not required for the proof, it is stated in the original paper. I don't know whether we should formalize this, or leave as a comment pointing at https://github.com/leanprover-community/mathlib4/pull/31960 as a key ingredient.