OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkStateMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The repeated fork state carries the original ordinary-spin Hamiltonian.

  1. def OAI.ContinuumCoulomb.QMAForkState.matrix line 16
  2. def OAI.ContinuumCoulomb.QMAForkState.retainedLeft line 19
  3. def OAI.ContinuumCoulomb.QMAForkState.retainedRight line 21
  4. def OAI.ContinuumCoulomb.QMAForkState.retainedWeight line 23
  5. def OAI.ContinuumCoulomb.QMAForkState.pairWeight line 27
  6. theorem OAI.ContinuumCoulomb.QMAForkState.retained_distinct line 30
  7. theorem OAI.ContinuumCoulomb.QMAForkState.matrix_pair_split line 36
  8. def OAI.ContinuumCoulomb.QMAForkState.nextWeight line 58
  9. def OAI.ContinuumCoulomb.QMAForkState.nextActive line 64
  10. def OAI.ContinuumCoulomb.QMAForkState.nextConstant line 70