OAI/Analysis/RieszRectifiability/Restart/CleanSupportPartition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Cleaning the support lattice partition

Removing the union of all cell overlaps produces nested, disjoint measurable cells that cover the support outside one exceptional set. Net centers avoid that set, so cleaning preserves the closed cells as closures. Under the growth bounds, it also preserves cell mass and gives a unique cell at every scale almost everywhere.

  1. def OAI.RieszRectifiability.supportLatticeExceptional line 22
  2. def OAI.RieszRectifiability.cleanSupportCell line 25
  3. theorem OAI.RieszRectifiability.supportLatticeExceptional_measurable line 29
  4. theorem OAI.RieszRectifiability.supportLatticeExceptional_null line 33
  5. theorem OAI.RieszRectifiability.cleanSupportCell_measurable line 41
  6. theorem OAI.RieszRectifiability.cleanSupportCell_disjoint line 47
  7. theorem OAI.RieszRectifiability.cleanSupportCell_nested line 55
  8. theorem OAI.RieszRectifiability.cleanSupportCell_cover line 61
  9. theorem OAI.RieszRectifiability.net_center_not_exceptional line 67
  10. theorem OAI.RieszRectifiability.center_mem_cleanSupportCell line 81
  11. theorem OAI.RieszRectifiability.cleanSupportCell_closure line 86
  12. theorem OAI.RieszRectifiability.cleanSupportCell_measure_eq line 97
  13. theorem OAI.RieszRectifiability.cleanSupportCell_ae_unique line 106