OAI/Analysis/RieszRectifiability/Restart/ActiveRegionSmallRadiusLowerArea.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.activeRegionLowScaleAreaFactor line 14
2. theorem OAI.RieszRectifiability.activeRegionLowScaleAreaFactor_pos line 18
3. theorem OAI.RieszRectifiability.activeRegionLowScaleAreaFactor_lt_top line 25
4. def OAI.RieszRectifiability.activeRegionSmallRadiusLowerAreaConstant line 31
5. theorem OAI.RieszRectifiability.activeRegionSmallRadiusLowerAreaConstant_pos line 35
6. theorem OAI.RieszRectifiability.activeRegionSmallRadiusLowerAreaConstant_lt_top line 41
7. theorem OAI.RieszRectifiability.active_region_low_stopping_scale_ball_area_ge line 63
8. theorem OAI.RieszRectifiability.active_region_limit_small_radius_ball_area_ge line 106