Zulip Chat Archive

Stream: maths

Topic: Preiss' theorem


Kevin Buzzard (May 11 2022 at 11:47):

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 (May 11 2022 at 14:12):

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.


Last updated: Dec 20 2023 at 11:08 UTC