OAI/MeasureTheory/Falconer/Angular/AngularCountMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.stripHitBound line 10
  2. theorem OAI.PlanarFalconer.sourceArcLength_strip_le_bound line 14
  3. theorem OAI.PlanarFalconer.stripCount_lintegral line 21
  4. theorem OAI.PlanarFalconer.stripCount_mean_bound line 39
  5. theorem OAI.PlanarFalconer.stripCount_exceptional_bound line 45
  6. theorem OAI.PlanarFalconer.planeDot_quarterTurn line 62
  7. theorem OAI.PlanarFalconer.parallelTestCount_as_strip line 66
  8. theorem OAI.PlanarFalconer.parallelGoodSet_compl_bound line 74
  9. theorem OAI.PlanarFalconer.projectionGoodSet_compl_bound line 88