OAI/Combinatorics/HoneycombCorridor/BoundaryFlux.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.mem_sourceExits line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_source_flux line 15
  3. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_source_weight_bound line 22
  4. theorem OAI.PolynomialVacuumBridge.Corridor.convex_boundary_flux line 43
  5. def OAI.PolynomialVacuumBridge.Corridor.bottomSource line 49
  6. def OAI.PolynomialVacuumBridge.Corridor.InStrip line 51
  7. def OAI.PolynomialVacuumBridge.Corridor.reachesDistance line 53
  8. def OAI.PolynomialVacuumBridge.Corridor.lateralMass line 56
  9. def OAI.PolynomialVacuumBridge.Corridor.lateralLengthMass line 61
  10. def OAI.PolynomialVacuumBridge.Corridor.FiniteLateralTail line 66
  11. def OAI.PolynomialVacuumBridge.Corridor.directionCode line 74
  12. theorem OAI.PolynomialVacuumBridge.Corridor.advance_direction line 78
  13. theorem OAI.PolynomialVacuumBridge.Corridor.terminal_direction line 84
  14. theorem OAI.PolynomialVacuumBridge.Corridor.right_cut_direction_one line 94
  15. theorem OAI.PolynomialVacuumBridge.Corridor.right_cut_direction_two line 100
  16. theorem OAI.PolynomialVacuumBridge.Corridor.convex_source_direction_turn line 106