OAI/MeasureTheory/Falconer/Estimates/RegularCoarseCells.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Heavy coarse cells selected by their original point counts. Both the coarse regularity and the fine mass retained in their union are quantitative.

  1. theorem OAI.Falconer.regular_coarse_cells line 11
  2. theorem OAI.Falconer.heavy_coarse_union_count line 39