OAI/MeasureTheory/Falconer/Measures/DistanceMeasure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.distanceWeight line 14
2. def OAI.PlanarFalconer.weightedDistance line 17
3. theorem OAI.PlanarFalconer.weightedDistance_mass line 20
4. theorem OAI.PlanarFalconer.weightedDistance_mass_bounds line 26
5. theorem OAI.PlanarFalconer.weightedDistance_positive_finite line 50
6. theorem OAI.PlanarFalconer.weightedDistance_carried line 58
7. theorem OAI.PlanarFalconer.product_carried line 68
8. theorem OAI.PlanarFalconer.positive_distance_volume_of_weighted_ac line 83