OAI/MeasureTheory/Falconer/Graphs/GraphGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.quarterTurn line 9
  2. def OAI.PlanarFalconer.planeDot line 10
  3. def OAI.PlanarFalconer.graphA line 11
  4. def OAI.PlanarFalconer.graphB line 12
  5. def OAI.PlanarFalconer.graphDerivative line 13
  6. def OAI.PlanarFalconer.graphDirection line 15
  7. theorem OAI.PlanarFalconer.planeDot_abs_le line 18
  8. theorem OAI.PlanarFalconer.quarterTurn_twice line 29
  9. theorem OAI.PlanarFalconer.norm_quarterTurn_add line 33
  10. theorem OAI.PlanarFalconer.graph_transverse_identity line 46
  11. theorem OAI.PlanarFalconer.graph_direction_transverse line 54
  12. theorem OAI.PlanarFalconer.graph_product_strip line 60