OAI/MeasureTheory/Falconer/Radial/OccupiedRadialTree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Occupied dyadic trees with a common full-measure source core

  1. def OAI.Falconer.DyadicCube.emptyTreeCells line 13
  2. def OAI.Falconer.DyadicCube.occupiedTreeCore line 18
  3. theorem OAI.Falconer.DyadicCube.emptyTreeCells_measurable line 22
  4. theorem OAI.Falconer.DyadicCube.emptyTreeCells_null line 28
  5. theorem OAI.Falconer.DyadicCube.occupiedTreeCore_measurable line 43
  6. theorem OAI.Falconer.DyadicCube.occupiedTreeCore_full line 47
  7. theorem OAI.Falconer.DyadicCube.occupiedTreeCore_cover line 59
  8. theorem OAI.Falconer.DyadicCube.occupied_parent line 70
  9. theorem OAI.Falconer.DyadicCube.occupied_center_bound line 81
  10. theorem OAI.Falconer.DyadicCube.occupied_diameter_bound line 90