OAI/Analysis/RieszRectifiability/Kernel/InnerAnnuli.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.innerDyadicAnnulus line 13
2. theorem OAI.RieszRectifiability.innerDyadicAnnulus_measurable line 16
3. theorem OAI.RieszRectifiability.innerDyadicAnnulus_disjoint line 21
4. theorem OAI.RieszRectifiability.iUnion_innerDyadicAnnulus line 36
5. theorem OAI.RieszRectifiability.innerDyadicAnnulus_subset_ball line 59
6. theorem OAI.RieszRectifiability.inverseDistancePow_bound_on_innerAnnulus line 67
7. theorem OAI.RieszRectifiability.inverseDistancePow_integrableOn_innerAnnulus line 76
8. theorem OAI.RieszRectifiability.singleton_null_of_globalGrowth line 88