OAI/Combinatorics/HoneycombCorridor/CollisionPhase.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.unusedSlot line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.turnUnit_not line 12
  3. theorem OAI.PolynomialVacuumBridge.Corridor.turnUnits_cons line 15
  4. theorem OAI.PolynomialVacuumBridge.Corridor.turnUnits_reverse line 19
  5. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_append line 23
  6. theorem OAI.PolynomialVacuumBridge.Corridor.turnAngle_sum line 27
  7. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_turnUnits line 35
  8. theorem OAI.PolynomialVacuumBridge.Corridor.collision_weights_conjugate line 43
  9. theorem OAI.PolynomialVacuumBridge.Corridor.collision_weights_cos line 48
  10. theorem OAI.PolynomialVacuumBridge.Corridor.numeric_unused_face line 61
  11. theorem OAI.PolynomialVacuumBridge.Corridor.contour_unused_face line 77
  12. def OAI.PolynomialVacuumBridge.Corridor.CollisionPhase line 90
  13. theorem OAI.PolynomialVacuumBridge.Corridor.collision_phase line 99