OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/ChargeTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact energy of a virtual hole and double occupancy

A single hop out of the singly occupied subspace creates one empty site and one doubly occupied site. The full long-range charge penalty on that configuration is exactly U - V i j, so intersite direct repulsion remains in the superexchange denominator.

  1. def OAI.ContinuumCoulomb.chargeTransferOccupation line 18
  2. theorem OAI.ContinuumCoulomb.chargeTransfer_deviation line 21
  3. theorem OAI.ContinuumCoulomb.chargeTransfer_weighted_sum line 32
  4. theorem OAI.ContinuumCoulomb.chargeTransfer_deviation_sq_sum line 40
  5. theorem OAI.ContinuumCoulomb.chargeTransfer_penalty line 53

    Source documentation

    All direct interactions except the hole-double interaction cancel.

    theorem chargeTransfer_penalty {m : ℕ} (U : ℝ) (V : Fin m → Fin m → ℝ)
    (hole double : Fin m) (hne : hole ≠ double)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0) :
    chargePenalty U V (chargeTransferOccupation hole double) = U - V hole double := by
…

    Mentions: OAI.ContinuumCoulomb.chargePenalty, OAI.ContinuumCoulomb.chargeTransferOccupation