Preiss' theorem

Stream: maths

[Kevin Buzzard]

I was talking to an analyst about mathlib and asked them to state a theorem which they used, to see if we could formalise the statement. They stated Preiss' theorem https://en.wikipedia.org/wiki/Hausdorff_density#Preiss'_theorem . Is it relatively straightforard to state this theorem in Lean? I don't know anywhere near enough about the measure theory side of things to have a clue.

[Jireh Loreaux]

First, I'm not the best person to answer this, so I could be wrong. I don't think we currently have the definitions of density of a measure in \R^n at a point, or of rectifiability of a set. That being said, I don't see any major issues to formalizing those definitions relatively easily, at which point I think it's possible to state Preiss' theorem.