OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGridPorts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Distinct entry and exit spin locations for every grid cell.

  1. def OAI.ContinuumCoulomb.qmaGridPort line 10
  2. theorem OAI.ContinuumCoulomb.qmaGridPort_cell line 14
  3. theorem OAI.ContinuumCoulomb.qmaGridPort_injective line 18
  4. theorem OAI.ContinuumCoulomb.qmaGridPort_ne_center line 30
  5. theorem OAI.ContinuumCoulomb.qmaExpandedPoint_injective line 36
  6. def OAI.ContinuumCoulomb.qmaDirectedPort line 42
  7. theorem OAI.ContinuumCoulomb.qmaDirectedPort_injective line 44
  8. theorem OAI.ContinuumCoulomb.qmaGridPort_bounds line 54