OAI/MeasureTheory/Falconer/Estimates/Assembly.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.exists_last_crossing line 11
2. theorem OAI.PlanarFalconer.last_crossing_tail line 26
3. theorem OAI.PlanarFalconer.min_step line 46
4. theorem OAI.PlanarFalconer.min_height_le line 55
5. theorem OAI.PlanarFalconer.outer_exponent_identity line 77
6. theorem OAI.PlanarFalconer.outer_profile_gain line 80
7. theorem OAI.PlanarFalconer.parameter_loss_bound line 96
8. theorem OAI.PlanarFalconer.entry_depth_bounds line 110