OAI/Analysis/RieszRectifiability/Kernel/DyadicAnnuli.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.dyadicAnnulus line 13
2. theorem OAI.RieszRectifiability.dyadicAnnulus_measurable line 16
3. theorem OAI.RieszRectifiability.dyadicAnnulus_subset_ball line 21
4. theorem OAI.RieszRectifiability.exterior_subset_iUnion_dyadicAnnulus line 26
5. theorem OAI.RieszRectifiability.dyadicAnnulus_measure_lt_top line 36
6. theorem OAI.RieszRectifiability.inverseDistancePow_bound_on_annulus line 43
7. theorem OAI.RieszRectifiability.inverseDistancePow_integrableOn_annulus line 52