OAI/MeasureTheory/Falconer/Incidence/PencilDirections.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Direction sets of separated pencils. The fixed multiplicity and regularity costs are proved from the original point-line incidence.

  1. theorem OAI.Falconer.pencil_slope_fiber_card line 14
  2. theorem OAI.Falconer.pencil_slope_card line 34
  3. theorem OAI.Falconer.pencil_slope_strip_card line 42
  4. theorem OAI.Falconer.pencil_slope_regular line 68