OAI/MeasureTheory/Falconer/Geometry/InactiveBinScales.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.dyadic_power_real line 7
2. def OAI.PlanarFalconer.graphUncappedAngularScale line 11
3. def OAI.PlanarFalconer.graphAngularScale line 14
4. theorem OAI.PlanarFalconer.graphUncappedAngularScale_pos line 17
5. theorem OAI.PlanarFalconer.graphAngularScale_pos line 22
6. theorem OAI.PlanarFalconer.graphAngularScale_cap_inactive line 25
7. theorem OAI.PlanarFalconer.inactive_bin_scale_slack line 44