Formalizing a result of Marstrand in geometric measure theor

Stream: general

[Ignacio Tejeda]

Hi there!

Me, @Theodore Meek , @Annie Cao , @joshua giir and @nathanp are trying to formalize the following theorem of Marstrand:

Marstrand.png

We are wondering if people here are interested in geometric measure theory or this result in particular. Specifically, we were wondering if this result is at a good level of generality for Mathlib, or if this should be a result contained in a separate GitHub. We would be happy to chat about this project and hear some feedback from more experienced people. Here is our repository: repo. So far we have proved 9 out of 11 lemmas needed, and upstreamed some basic lemmas: PR 1, PR 2. We are part of the UW Math AI Lab.

[Yongxi Lin (Aaron)]

I skimmed through your repo and it seems like your group only proves a weaker version of Marstrand theorem. Is the more general version significantly harder to prove? If you want sth to appear in Mathlib you should always try to prove the most general version.

Another thing that your group can improve is to write better definitions. For example, I don't see the point of the definition hausdorffContent right now (my understanding is that it is used in the construction of the Hausdorff measure in paper math but we already have Hausdorff measure in mathlib and we also have MeasureTheory.Measure.hausdorffMeasure_apply, is it possible to make your proof not depending on this new definition?) densityRatio certainly shouldn't be defined only for Hausdorff measures (and maybe one should first write some APIs to make this definition easy to use). Ds is really the lower s-density and there's no need to mention that the lower s-density is equal to the s-density in the definition of HasDs.

Also it seems like that your group used Aristotle a lot. Indeed Aristotle right now is powerful enough to solve some goals, but they often do it in an undesirable, overly complicated way. You need to improve the coding style (https://leanprover-community.github.io/contribute/style.html) and try to golf your proof (this is also why we want to go for more abstract theorems sometimes, abstraction may increase the diffculty of understanding but it reduces repetitive works in coding and may give you an easier way to formalize). This can increase the chances that your PRs to be accepted by Mathlib.

Overall I still found your project interesting. I am happy to help. Let me know if you need want to chat further.

[Ignacio Tejeda]

Thank you for your feedback! The version of Marstrand’s theorem we are trying to prove considers sets of dimensions between 0 and 1. The more general version, that applies to arbitrary positive dimensions, has a significantly different and longer proof. Formalizing that proof is something we would like to do. 

We are starting to clean-up our code - these guidelines will help a lot. For Hausdorff content, having a definition seems convenient math-wise, since it shows up in quite a few scenarios separately from the definition of Hausdorff measure. Given the fact that it is such a useful tool, proof-wise, we believe that formalizing the definition into mathlib would be of good use.

It seems that the definition of density of a Radon measure as considered in the setting of rectifiability (the one we use) is not available in mathlib, as opposed to densities between two Radon measures. This is something we will work on.

We would love to keep chatting with you about this. I can send you a DM.