OAI/Analysis/RieszRectifiability/Projections/ContractingProjectionRegions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Contracting projection regions

Local surface flatness and projection coverage select a stopping region whose representatives are quantitatively separated by projection. The core-area and stop-shadow estimates control the mass of its stopping cells.

  1. theorem OAI.RieszRectifiability.exists_contracting_projection_region line 23