OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListMerge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Canonical merging of a finite bond tape. A quadratic table of vertex pairs gives a deterministic order and retains exactly the pairs occurring in the input.

  1. abbrev OAI.ContinuumCoulomb.QuantumListMerge.Pair line 14
  2. def OAI.ContinuumCoulomb.QuantumListMerge.ordered line 16
  3. def OAI.ContinuumCoulomb.QuantumListMerge.pairs line 17
  4. def OAI.ContinuumCoulomb.QuantumListMerge.support line 18
  5. def OAI.ContinuumCoulomb.QuantumListMerge.weight line 20
  6. def OAI.ContinuumCoulomb.QuantumListMerge.value line 22
  7. theorem OAI.ContinuumCoulomb.QuantumListMerge.pairs_nodup line 25
  8. theorem OAI.ContinuumCoulomb.QuantumListMerge.pairs_length line 28
  9. theorem OAI.ContinuumCoulomb.QuantumListMerge.support_nodup line 32
  10. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_length line 35
  11. theorem OAI.ContinuumCoulomb.QuantumListMerge.ordered_bounded line 39
  12. theorem OAI.ContinuumCoulomb.QuantumListMerge.mem_support line 43
  13. theorem OAI.ContinuumCoulomb.QuantumListMerge.bounded line 54
  14. theorem OAI.ContinuumCoulomb.QuantumListMerge.noLoops line 61
  15. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_get line 71