OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumReferenceTerms.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The full reference Hamiltonian as explicit bounded-support real terms.

  1. abbrev OAI.ContinuumCoulomb.QMAReferenceTerm line 13
  2. def OAI.ContinuumCoulomb.qmaReferenceTermMatrix line 15
  3. def OAI.ContinuumCoulomb.qmaReferenceTermSites line 21
  4. def OAI.ContinuumCoulomb.qmaReferenceOnQubits line 26
  5. theorem OAI.ContinuumCoulomb.qmaReferenceTerm_sum line 32
  6. theorem OAI.ContinuumCoulomb.qmaReferenceTerm_local line 46
  7. theorem OAI.ContinuumCoulomb.qmaReferenceTerm_card line 56
  8. theorem OAI.ContinuumCoulomb.qmaReferenceTerm_hermitian line 72
  9. theorem OAI.ContinuumCoulomb.qmaReferenceTerm_real line 80