OAI/Analysis/RieszRectifiability/Projections/ProjectionRegionDepthCharts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-depth projection-region charts

Iterating child assembly yields a bounded chart with recursively controlled Lipschitz constant. A fixed fractional stop-mass bound gives a geometric uncovered-mass bound at each finite depth.

  1. def OAI.RieszRectifiability.projectionRegionDepthConstant line 21
  2. theorem OAI.RieszRectifiability.exists_projection_region_depth_chart line 25