OAI/Analysis/LipschitzHilbert/Geometry/ProjectionGroupSelection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite maximal-length grouping of overlapping projected popularity sets used in the far-angle estimate.

  1. def OAI.LipschitzHilbert.projectionBlocked line 13
  2. theorem OAI.LipschitzHilbert.projectionBlocked_mono line 17
  3. theorem OAI.LipschitzHilbert.projection_group_run_exists line 22
  4. theorem OAI.LipschitzHilbert.RectangleCoverRun.selected_unblocked_before line 31
  5. theorem OAI.LipschitzHilbert.RectangleCoverRun.projected_centers_disjoint line 42
  6. theorem OAI.LipschitzHilbert.RectangleCoverRun.projected_center_cover line 55