OAI/MeasureTheory/Falconer/Incidence/PacketRowPencils.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lift actual projected row points back to their original fine-scale pencils inside a coarse packet. Dilation preserves each pencil cardinality and the whole new union is contained in the dilation of the original union.

  1. theorem OAI.Falconer.packet_row_pencil_lift line 11