OAI/Analysis/RieszRectifiability/Foundations/NoncollapsingRegionRepresentatives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Projection separation of region representatives

A good cell containing two region representatives supplies a common fitted plane. Its noncollapsing projection estimate and the tube error bound give quantitative separation of the representatives after projection.

  1. theorem OAI.RieszRectifiability.projection_separates_noncollapsing_region_representatives line 22
  2. theorem OAI.RieszRectifiability.exists_cover_of_noncollapsing_region_representatives line 56