OAI/MeasureTheory/Falconer/Estimates/PositiveDistanceWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.PositiveDistanceData.spatialWeight line 10
2. theorem OAI.PlanarFalconer.PositiveDistanceData.measurable_spatialWeight line 13
3. theorem OAI.PlanarFalconer.PositiveDistanceData.spatialWeight_nonneg line 19
4. def OAI.PlanarFalconer.PositiveDistanceData.StronglySeparated line 24
5. theorem OAI.PlanarFalconer.PositiveDistanceData.stronglySeparated_of_unit line 30
6. theorem OAI.PlanarFalconer.PositiveDistanceData.separated_distance_ratio line 41
7. theorem OAI.PlanarFalconer.PositiveDistanceData.spatialWeight_le_one line 53
8. theorem OAI.PlanarFalconer.PositiveDistanceData.spatialWeight_lower line 63
9. theorem OAI.PlanarFalconer.PositiveDistanceData.ae_cellPair_mem line 72
10. theorem OAI.PlanarFalconer.PositiveDistanceData.ae_spatialWeight_bounds line 80