OAI/MeasureTheory/Falconer/Angular/CappedActiveCover.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded anchor lists for every original direction label

  1. def OAI.Falconer.cappedActiveAnchors line 14
  2. theorem OAI.Falconer.cappedActiveAnchors_card line 19
  3. theorem OAI.Falconer.cappedActiveAnchors_eq line 27
  4. theorem OAI.Falconer.gaussian_capped_coordinate_cover line 35