OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumReferenceEdges.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The reference alignment penalty is a sum of real two-site interactions.

  1. def OAI.ContinuumCoulomb.qmaReferenceYEdge line 14
  2. theorem OAI.ContinuumCoulomb.qmaReferenceYEdge_local line 18
  3. theorem OAI.ContinuumCoulomb.qmaReferenceYEdge_real line 29
  4. theorem OAI.ContinuumCoulomb.qmaReferenceYEdge_hermitian line 36
  5. def OAI.ContinuumCoulomb.qmaReferenceEdgeOnQubits line 50
  6. def OAI.ContinuumCoulomb.qmaReferenceEdgeSites line 54
  7. theorem OAI.ContinuumCoulomb.qmaReferenceEdgeOnQubits_local line 57
  8. theorem OAI.ContinuumCoulomb.qmaReferenceEdgeOnQubits_real line 63
  9. theorem OAI.ContinuumCoulomb.qmaReferenceEdgeOnQubits_hermitian line 70