OAI/Analysis/RieszRectifiability/Foundations/ADHoleDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

AD lower bounds and global upper growth quantify the density lost to a ball-shaped hole. Persistent holes at vanishing scales force a measurable set to have zero measure.

  1. def OAI.RieszRectifiability.ballHoleDensityDefect line 18
  2. theorem OAI.RieszRectifiability.ballHoleDensityDefect_pos line 20
  3. theorem OAI.RieszRectifiability.ad_ball_hole_density_bound line 25
  4. theorem OAI.RieszRectifiability.measurable_set_null_of_uniform_ball_holes line 75