OAI/MeasureTheory/Falconer/Geometry/ProjectionBuffer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Directional buffers for the actual full-law projection test

  1. theorem OAI.Falconer.projectionCollision_direction_transfer line 12
  2. theorem OAI.Falconer.projectionGoodSet_buffer line 31