OAI/MeasureTheory/Falconer/Geometry/ScalarGridProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An actual coefficient from the dyadic grid gives a large scalar projection. All constants come from the finite collision estimate.

  1. theorem OAI.Falconer.dense_projection_obstruction_divide line 10
  2. theorem OAI.Falconer.scalar_grid_large_projection line 23