Question about background

Stream: Carleson

[Bolton Bailey]

I was looking at this lemma marked as "ready to be formalized". It seems like it relies on the concept of "doubling metric measure space". The closest thing in mathlib seems to be docs#IsUnifLocDoublingMeasure, which doesn't seem exactly the same as the description I see on wikipedia - are we still looking for a formalization of the "doubling metric measure space" concept?

[Pietro Monticone]

See here.

[Bolton Bailey]

Thanks! Second question: Is it possible to claim this task? I don't see it on the outstanding tasks list, but perhaps I can just complete it and make a PR for it anyway?

[Floris van Doorn]

I think the lemma you linked is essentially already in Mathlib.
For the formalization I was mostly focusing on proving the general result, but of course I would also like help on chapters 10 and 11 at some point. I'm planning to go through these chapters myself and state all the results.
If you want to help with this, the most helpful contribution at the moment would be to start stating all lemmas in some section (or multiple) of chapters 10/11.