OAI/MeasureTheory/Falconer/Angular/ActualAngularTests.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.stripCount line 11
  2. theorem OAI.PlanarFalconer.measurable_stripCount line 16
  3. theorem OAI.PlanarFalconer.stripCount_neg line 33
  4. theorem OAI.PlanarFalconer.stripCount_transfer line 39
  5. def OAI.PlanarFalconer.parallelTestCells line 58
  6. def OAI.PlanarFalconer.projectionTestCells line 64
  7. def OAI.PlanarFalconer.parallelTestCount line 69
  8. def OAI.PlanarFalconer.projectionTestCount line 74
  9. def OAI.PlanarFalconer.parallelGoodSet line 79
  10. def OAI.PlanarFalconer.projectionGoodSet line 83
  11. theorem OAI.PlanarFalconer.continuous_quarterTurn line 87
  12. theorem OAI.PlanarFalconer.norm_quarterTurn line 91
  13. theorem OAI.PlanarFalconer.quarterTurn_sub line 94

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Graphs/GraphChartVariation.lean:9 (different declaration text). Qualify references as OAI.PlanarFalconer.quarterTurn_sub@path.

  14. theorem OAI.PlanarFalconer.measurable_parallelGoodSet line 99
  15. theorem OAI.PlanarFalconer.measurable_projectionGoodSet line 106
  16. theorem OAI.PlanarFalconer.parallelTestCount_neg line 112
  17. theorem OAI.PlanarFalconer.projectionTestCount_neg line 119
  18. theorem OAI.PlanarFalconer.parallelTestCount_transfer line 124
  19. theorem OAI.PlanarFalconer.projectionTestCount_transfer line 136