OAI/Analysis/RieszRectifiability/Nets/LatticeDescendantGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RieszRectifiability.SupportCellDescendant line 13
  2. def OAI.RieszRectifiability.SupportCellDescendant.radius line 23
  3. def OAI.RieszRectifiability.SupportCellDescendant.binaryLevel line 25
  4. def OAI.RieszRectifiability.SupportCellDescendant.cell line 27
  5. theorem OAI.RieszRectifiability.SupportCellDescendant.radius_pos line 30
  6. theorem OAI.RieszRectifiability.SupportCellDescendant.center_mem_support line 33
  7. theorem OAI.RieszRectifiability.SupportCellDescendant.center_dist_top line 36
  8. theorem OAI.RieszRectifiability.SupportCellDescendant.binary_radius line 43
  9. theorem OAI.RieszRectifiability.SupportCellDescendant.scale_eq line 52
  10. theorem OAI.RieszRectifiability.SupportCellDescendant.separated line 58
  11. theorem OAI.RieszRectifiability.SupportCellDescendant.core_admissible line 78
  12. theorem OAI.RieszRectifiability.SupportCellDescendant.cell_subset_top line 87