OAI/MeasureTheory/Falconer/Incidence/UniformFrozenCells.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original uniform fine pencils produce frozen coarse cells at every intermediate scale. The point restrictions have explicit logarithmic costs.

  1. theorem OAI.Falconer.uniform_frozen_cells line 14