OAI/MeasureTheory/Falconer/Geometry/SeparatedDistanceMaximum.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFalconer.filtered_pair_sum_le_degreeline 10 - def
OAI.PlanarFalconer.PositiveDistanceData.separatedMaximumline 35 - theorem
OAI.PlanarFalconer.PositiveDistanceData.separatedMaximum_ne_topline 40 - theorem
OAI.PlanarFalconer.PositiveDistanceData.separated_sum_le_degreeline 49 - theorem
OAI.PlanarFalconer.PositiveDistanceData.separated_sum_le_maximumline 58