OAI/Analysis/RieszRectifiability/Restart/CellRegionStopping.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Limits and stops of good cell regions

The limit region consists of points whose containing descendants all satisfy a chosen good-cell predicate. Stops are the first failures along containment chains. Countability of descendants makes the limit region measurable by removing the union of bad cells from the starting cell.

  1. def OAI.RieszRectifiability.cellRegionLimit line 22
  2. def OAI.RieszRectifiability.cellRegionStops line 27
  3. theorem OAI.RieszRectifiability.cellRegionLimit_measurable line 33
  4. theorem OAI.RieszRectifiability.exists_first_failing_cell line 55
  5. theorem OAI.RieszRectifiability.cellRegionStops_pairwise_disjoint line 77
  6. theorem OAI.RieszRectifiability.cellRegionLimit_disjoint_stops line 89
  7. theorem OAI.RieszRectifiability.cleanSupportCell_eq_region_limit_union_stops line 98