OAI/MeasureTheory/Falconer/Incidence/FinerPencilDirections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Good projected directions at the finer scale used by a dilated coarse packet. The ratio eight is the actual fixed packet-width margin.

  1. theorem OAI.Falconer.good_pencil_projection_directions_finer line 11