OAI/Analysis/LipschitzHilbert/Geometry/RectangleCoverSelection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite selection with the exact length/eccentricity priority in the Lacey--Li covering algorithm. The removal predicate will be instantiated by containment in the auxiliary maximal-function level set.

  1. def OAI.LipschitzHilbert.rectanglePriority line 13
  2. theorem OAI.LipschitzHilbert.rectangle_priority_exists line 17
  3. def OAI.LipschitzHilbert.rectangleRemaining line 34
  4. theorem OAI.LipschitzHilbert.mem_rectangleRemaining line 39
  5. theorem OAI.LipschitzHilbert.rectangleRemaining_subset line 45
  6. theorem OAI.LipschitzHilbert.rectangleRemaining_card_lt line 50
  7. inductive OAI.LipschitzHilbert.RectangleCoverRun line 61
  8. theorem OAI.LipschitzHilbert.rectangle_cover_run_exists line 71
  9. theorem OAI.LipschitzHilbert.RectangleCoverRun.selected_subset line 96
  10. theorem OAI.LipschitzHilbert.RectangleCoverRun.selected_nodup line 106
  11. theorem OAI.LipschitzHilbert.RectangleCoverRun.selected_priority line 116
  12. theorem OAI.LipschitzHilbert.RectangleCoverRun.rejected_blocked line 127