OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorOnsite.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Internal physical exchanges encode the one-site and scalar X/Z terms.

  1. def OAI.ContinuumCoulomb.qmaFourTensorFields line 13
  2. def OAI.ContinuumCoulomb.qmaFourTensorFieldShift line 17
  3. def OAI.ContinuumCoulomb.qmaFourTensorOnsite line 20
  4. theorem OAI.ContinuumCoulomb.qmaFourTensorOnsite_compression line 24
  5. theorem OAI.ContinuumCoulomb.qmaFourTensorFields_star line 35
  6. theorem OAI.ContinuumCoulomb.qmaFourTensorOnsite_star line 39
  7. theorem OAI.ContinuumCoulomb.qmaFourTensorFields_norm line 45
  8. theorem OAI.ContinuumCoulomb.qmaFourAxisFieldShift_abs line 50
  9. theorem OAI.ContinuumCoulomb.qmaFourTensorFieldShift_abs line 57
  10. theorem OAI.ContinuumCoulomb.qmaFourTensorOnsite_norm line 62