OAI/Combinatorics/HoneycombCorridor/RationalPotential.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialVacuumBridge.Corridor.QFlow.FaceIndex line 9
  2. def OAI.PolynomialVacuumBridge.Corridor.QFlow.facePrefix line 11
  3. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.facePrefix_difference line 14
  4. def OAI.PolynomialVacuumBridge.Corridor.QFlow.InFaceBox line 38
  5. def OAI.PolynomialVacuumBridge.Corridor.QFlow.faceRadius line 41
  6. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.mem_support_in_box line 44
  7. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.facePrefix_left_zero line 53
  8. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.facePrefix_row_zero line 62
  9. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.int_function_constant line 72
  10. structure OAI.PolynomialVacuumBridge.Corridor.QFlow.FiniteHoneycombFlow line 83
  11. def OAI.PolynomialVacuumBridge.Corridor.QFlow.flowPotential line 90
  12. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.flow_difference line 93
  13. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.flowPotential_vertical line 99
  14. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.flowPotential_right_zero line 127
  15. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.flowPotential_finite_support line 144
  16. def OAI.PolynomialVacuumBridge.Corridor.QFlow.finiteFlowPotential line 166
  17. theorem OAI.PolynomialVacuumBridge.Corridor.QFlow.finite_flow_is_face_boundary line 170