OAI/MeasureTheory/Falconer/Recursion/RecursiveCellInvariants.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.PositiveDistanceData.RecursiveCells line 11
2. theorem OAI.PlanarFalconer.PositiveDistanceData.RecursiveCells.stronglySeparated line 16
3. theorem OAI.PlanarFalconer.PositiveDistanceData.RecursiveCells.update line 20
4. theorem OAI.PlanarFalconer.PositiveDistanceData.angularSuccessor_lengths line 23
5. theorem OAI.PlanarFalconer.PositiveDistanceData.angularSuccessor_budget line 35
6. theorem OAI.PlanarFalconer.AngularStateData.successor_budget line 46
7. theorem OAI.PlanarFalconer.AngularStateData.far_recursive_cells line 52
8. theorem OAI.PlanarFalconer.AngularStateData.far_atCells_branchState line 62
9. theorem OAI.PlanarFalconer.AngularStateData.far_atCells_profile line 65