OAI/MeasureTheory/Falconer/Geometry/DyadicGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarFalconer.DyadicSquare line 12
2. def OAI.PlanarFalconer.DyadicSquare.carrier line 17
3. def OAI.PlanarFalconer.DyadicSquare.child line 21
4. theorem OAI.PlanarFalconer.DyadicSquare.child_side_pos line 25
5. theorem OAI.PlanarFalconer.DyadicSquare.measurable line 30
6. theorem OAI.PlanarFalconer.DyadicSquare.child_subset line 38
7. theorem OAI.PlanarFalconer.DyadicSquare.cover_children line 48
8. theorem OAI.PlanarFalconer.DyadicSquare.children_disjoint line 68
9. theorem OAI.PlanarFalconer.DyadicSquare.dist_le line 77
10. theorem OAI.PlanarFalconer.DyadicSquare.ediam_le line 92