OAI/MeasureTheory/Falconer/Geometry/ScalarGridFibers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar dyadic cell fibers for the porous grouping step.

  1. def OAI.Falconer.scalarGridFiber line 9
  2. theorem OAI.Falconer.scalarGridFiber_mono line 12
  3. theorem OAI.Falconer.scalarGridFiber_small line 16
  4. theorem OAI.Falconer.scalarGridFiber_double_subset line 29
  5. theorem OAI.Falconer.scalarGridFiber_double_card line 44
  6. theorem OAI.Falconer.scalarGridFiber_wide line 49
  7. theorem OAI.Falconer.scalar_grid_sum line 57