OAI/MeasureTheory/Falconer/Incidence/CenteredPacketPencils.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lift projected rows directly from an arbitrary original coarse packet. Affine centering and dilation preserve the original union cardinality.

  1. theorem OAI.Falconer.centered_packet_pencil_lift line 10