OAI/MeasureTheory/Falconer/Recursion/BlockLeafCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.blockBin line 8
2. def OAI.PlanarFalconer.blockProduct line 12
3. theorem OAI.PlanarFalconer.blockBin_pos line 15
4. theorem OAI.PlanarFalconer.blockProduct_pos line 19
5. theorem OAI.PlanarFalconer.blockBin_le line 23
6. theorem OAI.PlanarFalconer.blockClass_child_bounds line 30
7. theorem OAI.PlanarFalconer.blockClass_leaf_count line 54
8. theorem OAI.PlanarFalconer.blockClass_root_count line 89