OAI/Analysis/LipschitzHilbert/Geometry/FarSlabExclusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The long-rectangle exclusion estimate (Lacey--Li, Lemma 3.16) from actual non-removal. The finite direction net is the one already used in the near-angle selection estimate.

  1. theorem OAI.LipschitzHilbert.long_slab_threshold line 13
  2. theorem OAI.LipschitzHilbert.far_slab_selected_bound line 18
  3. theorem OAI.LipschitzHilbert.comparable_slab_threshold line 67
  4. theorem OAI.LipschitzHilbert.comparable_slab_selected_bound line 72