OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListMergeMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Canonical bond merging preserves the complete exchange matrix exactly.

  1. theorem OAI.ContinuumCoulomb.QuantumListMerge.sum_indicator line 12
  2. theorem OAI.ContinuumCoulomb.QuantumListMerge.sum_swap line 33
  3. theorem OAI.ContinuumCoulomb.QuantumListMerge.ordered_matrix line 43
  4. theorem OAI.ContinuumCoulomb.QuantumListMerge.pairMatrix_add line 55
  5. theorem OAI.ContinuumCoulomb.QuantumListMerge.pairMatrix_contribution line 61
  6. theorem OAI.ContinuumCoulomb.QuantumListMerge.matrix_row line 71
  7. theorem OAI.ContinuumCoulomb.QuantumListMerge.matrix_eq line 84