OAI/MeasureTheory/Falconer/Graphs/WeightedDistanceCoincidence.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFalconer.PositiveDistanceData.weighted_lower_constant_sqline 11 - theorem
OAI.PlanarFalconer.PositiveDistanceData.normalization_weighted_identityline 21 - theorem
OAI.PlanarFalconer.PositiveDistanceData.weightedDistance_collision_lowerline 27 - theorem
OAI.PlanarFalconer.PositiveDistanceData.coincidence_le_weighted_collisionline 42