OAI/MeasureTheory/Falconer/Estimates/ActualSuccessorUpperBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.finiteEnergyMaximum_le line 9
2. theorem OAI.PlanarFalconer.PositiveDistanceData.prefixLowMaximum_le line 21
3. theorem OAI.PlanarFalconer.PositiveDistanceData.prefixSuccessorSupremum_le line 26
4. theorem OAI.PlanarFalconer.PositiveDistanceData.prefixSuccessorEnergies_mono line 42
5. theorem OAI.PlanarFalconer.PositiveDistanceData.separatedMaximum_le_ofReal line 50
6. theorem OAI.PlanarFalconer.PositiveDistanceData.separatedMaximum_toReal_le line 69
7. theorem OAI.PlanarFalconer.AngularStateData.childMaximum_le line 83
8. theorem OAI.PlanarFalconer.AngularStateData.farDistanceMaximum_le line 89
9. theorem OAI.PlanarFalconer.AngularStateData.farSum_le_card line 99
10. theorem OAI.PlanarFalconer.AngularStateData.farSum_le_depth_factor line 106