OAI/MeasureTheory/Falconer/Geometry/ProjectionLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar projection law and its sinc collision bound

  1. def OAI.Falconer.scalarProjectionLaw line 13
  2. instance OAI.Falconer.scalarProjectionLaw_finite line 16
  3. theorem OAI.Falconer.charFun_scalarProjectionLaw line 19
  4. theorem OAI.Falconer.norm_charFun_scalarProjectionLaw line 27
  5. def OAI.Falconer.projectionCollision line 36
  6. theorem OAI.Falconer.scalarProjectionLaw_collision line 39
  7. theorem OAI.Falconer.projection_collision_fourier line 50