OAI/MeasureTheory/Falconer/Incidence/CoarseCellPencils.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct all coarse cell pencils from the original fine incidences, with one common logarithmic loss and their original fine witnesses.

  1. theorem OAI.Falconer.coarse_cell_pencils line 11