Geometric measure theory

Stream: Is there code for X?

[Adhyayan Sharma]

Hey everyone! I'm looking to formalise a small result in geometric measure theory, are there any concepts from GMT (e.g., coarea formula, radon measures) that have been formalised in mathlib?

is there anyone working on this by any chance, id be keen to get involved with formalising some GMT, and collaborate on tasks if anyone is interested :D

[Jireh Loreaux]

There's lots of GMT in the Carleson project, I'm sure.

[Adhyayan Sharma]

I'll try to go through that, thanks!