OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLatticeSource.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Convert an actual simple rational grid graph into the field-free source Hamiltonian, retaining the exact scalar shift in its thresholds.

  1. def OAI.ContinuumCoulomb.qmaGridCoordinate line 14
  2. theorem OAI.ContinuumCoulomb.qmaGridCoordinate_injective line 16
  3. theorem OAI.ContinuumCoulomb.qmaNatDistance line 22
  4. theorem OAI.ContinuumCoulomb.qmaGridCoordinate_adj line 27
  5. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.Simple line 35
  6. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_simple line 39
  7. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.latticeSource line 50
  8. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.latticeSource_matrix line 68
  9. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.latticeSource_energy line 84