OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBufferedLanes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Eightfold lane spacing leaves room for the buffered endpoint arms.

  1. def OAI.ContinuumCoulomb.qmaSpacedLaneColor line 11
  2. theorem OAI.ContinuumCoulomb.qmaSpacedLaneColor_injective line 13
  3. theorem OAI.ContinuumCoulomb.qmaSpacedEndpoint line 20
  4. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.spacedColor line 28
  5. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.spacedSupport line 31
  6. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.spacedColor_eq line 35
  7. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.spaced_color_disjoint line 41
  8. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.spaced_length line 61
  9. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.spaced_crossing_not_vertex line 68