OAI/MeasureTheory/Falconer/Radial/CoarsePlateCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact product-cell structure of every finite coarse plate filter

  1. theorem OAI.Falconer.DyadicCube.descendant_subset_take line 10
  2. theorem OAI.Falconer.DyadicCube.same_fine_cell_coarse line 18
  3. theorem OAI.Falconer.heavyPlateCellPairs_fine_invariant line 31
  4. theorem OAI.Falconer.coarsePlateFilter_fine_invariant line 44
  5. theorem OAI.Falconer.coarsePlateFilter_product_cells line 58