OAI/Analysis/RieszRectifiability/Nets/SupportCellOverlaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Null overlaps of support lattice cells

The countable union of intersections of distinct closed cells is measurable and avoids every deep core ball. Upper growth and lower AD bounds turn these holes into nullity; when a core radius exceeds the support diameter, separation makes the overlap empty.

  1. def OAI.RieszRectifiability.supportLatticeOverlap line 22
  2. theorem OAI.RieszRectifiability.mem_supportLatticeOverlap line 28
  3. theorem OAI.RieszRectifiability.supportLatticeOverlap_measurable line 42
  4. theorem OAI.RieszRectifiability.supportLatticeOverlap_subset_support line 56
  5. theorem OAI.RieszRectifiability.supportLatticeOverlap_disjoint_deep_core line 62
  6. theorem OAI.RieszRectifiability.supportLatticeOverlap_null_of_admissible_core line 73
  7. theorem OAI.RieszRectifiability.supportLatticeOverlap_null line 96