OAI/Analysis/RieszRectifiability/Restart/ProjectionStopShadowMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Projected mass of stopping-cell shadows

The stopping-cell radius bound converts individual fitted-plane shadow estimates into a Hausdorff measure bound for their projected union, controlled by the top cell's mass.

  1. def OAI.RieszRectifiability.projectionStopShadowConstant line 21
  2. theorem OAI.RieszRectifiability.cellRegion_stopping_radius_power_le_top line 25
  3. theorem OAI.RieszRectifiability.projection_conditioned_stopping_shadow_le_top line 44