OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedHubbard.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual localized direct Coulomb matrix satisfies the full charge penalty condition used by the complete half-filled Hubbard comparison.

  1. def OAI.ContinuumCoulomb.localizedOffsiteCoulomb line 13
  2. theorem OAI.ContinuumCoulomb.localizedOffsiteCoulomb_diagonal line 16
  3. theorem OAI.ContinuumCoulomb.localizedOffsiteCoulomb_symmetric line 19
  4. theorem OAI.ContinuumCoulomb.localizedCoulomb_diagonal_split line 25
  5. theorem OAI.ContinuumCoulomb.localizedCoulomb_charge_condition line 47
  6. theorem OAI.ContinuumCoulomb.HubbardGlobal.localized_hubbard_Heisenberg line 58
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.localized_calibrated_hubbard line 81