OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumMergeEdges.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Parallel interactions are combined at one canonically ordered physical edge. This is an exact matrix operation, with no perturbative error.

  1. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.orderedPair line 13
  2. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.edgePairs line 16
  3. abbrev OAI.ContinuumCoulomb.QMARationalExchangeGraph.MergedEdge line 19
  4. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.edgeClass line 21
  5. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.orderedPair_lt line 24
  6. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.mergedEdge_lt line 30
  7. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.orderedPair_matrix line 35
  8. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge line 43
  9. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_matrix line 52
  10. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_energy line 72
  11. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_pair_injective line 77
  12. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_edge_count line 82
  13. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_edge_source line 87