OAI/MeasureTheory/Falconer/Estimates/WeightedDistancePushforward.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.PositiveDistanceData.weightedPair line 12
2. def OAI.PlanarFalconer.PositiveDistanceData.weightedDistance line 15
3. theorem OAI.PlanarFalconer.PositiveDistanceData.weightedPair_le line 18
4. theorem OAI.PlanarFalconer.PositiveDistanceData.weightedPair_isFinite line 27
5. theorem OAI.PlanarFalconer.PositiveDistanceData.weightedDistance_isFinite line 34
6. theorem OAI.PlanarFalconer.PositiveDistanceData.weightedPair_lower line 40
7. theorem OAI.PlanarFalconer.PositiveDistanceData.weightedDistance_lower line 53
8. theorem OAI.PlanarFalconer.PositiveDistanceData.lintegral_weightedDistance line 62
9. theorem OAI.PlanarFalconer.PositiveDistanceData.integral_weightedDistance line 73