OAI/MeasureTheory/Falconer/Estimates/PacketCentering.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Center a genuine coarse line packet by an affine shear. Translation in line-parameter space preserves all pencil counts and ball bounds exactly; the point-line residual is unchanged.

  1. def OAI.Falconer.packetCenterPoint line 11
  2. def OAI.Falconer.packetCenterLine line 14
  3. theorem OAI.Falconer.packetCenterPoint_inverse line 17
  4. theorem OAI.Falconer.packetCenterPoint_injective line 25
  5. theorem OAI.Falconer.packetCenterLine_inverse line 29
  6. theorem OAI.Falconer.packetCenterLine_injective line 38
  7. theorem OAI.Falconer.packetCenterLine_dist line 42
  8. theorem OAI.Falconer.packetCenterLine_card line 52
  9. theorem OAI.Falconer.packetCenterLine_separated line 56
  10. theorem OAI.Falconer.packetCenterLine_regular line 64
  11. theorem OAI.Falconer.packetCenter_residual line 82
  12. theorem OAI.Falconer.packetCenter_residual_le line 88
  13. theorem OAI.Falconer.local_centered_projection line 95