OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListMergeProperties.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The merged tape has one strictly ordered edge per occurring vertex pair, and its coefficients grow by at most the original edge count.

  1. def OAI.ContinuumCoulomb.QuantumListMerge.supportIndex line 12
  2. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_pair line 15
  3. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_pair_injective line 20
  4. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_ordered line 28
  5. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_simple line 37
  6. theorem OAI.ContinuumCoulomb.QuantumListMerge.weight_abs_le line 51