OAI/MeasureTheory/Falconer/Estimates/PositiveDistancePushforward.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PlanarFalconer.PositiveDistanceData line 10
  2. def OAI.PlanarFalconer.PositiveDistanceData.good line 27
  3. theorem OAI.PlanarFalconer.PositiveDistanceData.measurable_good line 30
  4. def OAI.PlanarFalconer.PositiveDistanceData.cellPair line 33
  5. def OAI.PlanarFalconer.PositiveDistanceData.pair line 37
  6. def OAI.PlanarFalconer.PositiveDistanceData.distance line 40
  7. instance OAI.PlanarFalconer.PositiveDistanceData.cellPair_finite line 43
  8. instance OAI.PlanarFalconer.PositiveDistanceData.pair_finite line 46
  9. instance OAI.PlanarFalconer.PositiveDistanceData.distance_finite line 49
  10. def OAI.PlanarFalconer.PositiveDistanceData.width line 52
  11. def OAI.PlanarFalconer.PositiveDistanceData.levelMass line 54
  12. def OAI.PlanarFalconer.PositiveDistanceData.normalization line 57
  13. def OAI.PlanarFalconer.PositiveDistanceData.coincidence line 60
  14. theorem OAI.PlanarFalconer.PositiveDistanceData.distance_apply line 64
  15. theorem OAI.PlanarFalconer.PositiveDistanceData.distance_prod line 70
  16. theorem OAI.PlanarFalconer.PositiveDistanceData.distance_collision line 78
  17. theorem OAI.PlanarFalconer.PositiveDistanceData.coincidence_four_point line 84
  18. theorem OAI.PlanarFalconer.PositiveDistanceData.lintegral_distance_prod line 91
  19. theorem OAI.PlanarFalconer.PositiveDistanceData.lintegral_drop_extra_restriction line 98