OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockSiteOneBody.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The spatial one-body matrix acts on both conserved spin modes and agrees with the actual graph hopping operator.

  1. def OAI.ContinuumCoulomb.HubbardGlobal.spinLift line 13
  2. def OAI.ContinuumCoulomb.HubbardGlobal.siteBilinear line 18
  3. def OAI.ContinuumCoulomb.HubbardGlobal.siteOneBody line 22
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_spinLift line 25
  5. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteOneBody_add line 46
  6. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteOneBody_sum line 50
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteOneBody_single line 60
  8. def OAI.ContinuumCoulomb.HubbardGlobal.graphHoppingMatrix line 69
  9. theorem OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_graphHopping line 74