OAI/MeasureTheory/Falconer/Geometry/ScalarGridGrouping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A dyadic grid scale with controlled maximal occupancy. This selects the local groups used to treat arbitrary branching at a porous level.

  1. theorem OAI.Falconer.scalar_grid_grouping_of_small_cells line 10
  2. theorem OAI.Falconer.scalar_grid_grouping line 52