OAI/Analysis/LipschitzHilbert/Geometry/LaceyLiSelectionCover.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual discarded-family covering estimate in the Lacey--Li selection algorithm. The remaining energy estimate is geometric.

  1. theorem OAI.LipschitzHilbert.rectangleCount_mono line 14
  2. def OAI.LipschitzHilbert.maximalBlocked line 19
  3. theorem OAI.LipschitzHilbert.maximalBlocked_mono line 23
  4. theorem OAI.LipschitzHilbert.not_maximalBlocked_empty line 29
  5. theorem OAI.LipschitzHilbert.rectangle_cover_run_maximal_exists line 43
  6. theorem OAI.LipschitzHilbert.maximal_selection_cover_bound line 50