OAI/MeasureTheory/Falconer/Angular/GoodProjectionDirections.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At least half of the original direction labels have bounded projected energy. No direction is replaced and the estimate is uniform over later subsets of the planar point set.

  1. theorem OAI.Falconer.finite_low_half line 12
  2. def OAI.Falconer.projectionEnergyBudget line 33
  3. theorem OAI.Falconer.projectionEnergyBudget_pos line 36
  4. theorem OAI.Falconer.good_projection_directions line 43