OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumMergedSupport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Canonical merging preserves exactly the unordered endpoint support. This includes edges whose merged coefficient is zero.

  1. theorem OAI.ContinuumCoulomb.qmaUnorderedPair_map line 13
  2. theorem OAI.ContinuumCoulomb.QuantumListMerge.ordered_endpointPair line 23
  3. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_edge_source line 30
  4. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_edge_target line 40
  5. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_support line 48
  6. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.orderedPair_endpointPair line 63
  7. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_unordered_source line 70
  8. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_unordered_target line 75
  9. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_support line 79
  10. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_nat_support line 90
  11. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_support_forward line 103
  12. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.merge_support_backward line 114
  13. theorem OAI.ContinuumCoulomb.QuantumListGraph.ofBonds_nat_support line 130
  14. theorem OAI.ContinuumCoulomb.QuantumListGraph.mergedTape_nat_support line 145