OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBlockHamiltonian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal exchange sums for the real-coefficient four-spin Hamiltonian.

  1. def OAI.ContinuumCoulomb.qmaFourEdgeLeft line 13
  2. def OAI.ContinuumCoulomb.qmaFourEdgeRight line 14
  3. theorem OAI.ContinuumCoulomb.qmaFourEdge_distinct line 16
  4. theorem OAI.ContinuumCoulomb.qmaFourPenalty_edgeSum line 19
  5. def OAI.ContinuumCoulomb.qmaBlockSourcePenalty line 27
  6. theorem OAI.ContinuumCoulomb.qmaBlockSourcePenalty_reindex line 32
  7. def OAI.ContinuumCoulomb.qmaBlockSourceField line 43
  8. theorem OAI.ContinuumCoulomb.qmaBlockSourceField_reindex line 50
  9. def OAI.ContinuumCoulomb.qmaBlockSourceAxisField line 57
  10. theorem OAI.ContinuumCoulomb.qmaBlockSourceAxisField_reindex line 61
  11. def OAI.ContinuumCoulomb.qmaBlockSourceCoupling line 67
  12. theorem OAI.ContinuumCoulomb.qmaBlockSourceCoupling_reindex line 74