OAI/MeasureTheory/Falconer/Incidence/OriginalPencilEqualization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Equalize the original pencils before the fixed geometric preparation. Only a logarithmic fraction of the original point set is lost.

  1. theorem OAI.Falconer.original_pencil_equalization line 12