FockChargePolynomial.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The density interaction and its counterterm on the full half-filled Fock sector, including the scalar off-site Coulomb shift.

def OAI.ContinuumCoulomb.HubbardGlobal.directChargeValue line 14
def OAI.ContinuumCoulomb.HubbardGlobal.siteChargeOperator line 20
theorem OAI.ContinuumCoulomb.HubbardGlobal.siteChargeOperator_basis line 26
theorem OAI.ContinuumCoulomb.HubbardGlobal.siteChargeOperator_eq_diagonal line 51
theorem OAI.ContinuumCoulomb.HubbardGlobal.siteChargeOperator_halfFilled line 63
Source documentation
The manuscript's scalar shift holds for every half-filled vector, including charge defects and arbitrary spectator spins.
```
theorem siteChargeOperator_halfFilled (m : ℕ) (U : ℝ)
    (V : Fin (m+1) → Fin (m+1) → ℝ) (hsymm : ∀ i j, V i j = V j i)
    (x : Space (2*m+1)) (hx : IsHalfFilled m x) :
    siteChargeOperator m U V x = chargePenaltyFock m U V x -
      (((1 / 2 : ℝ) * ∑ i, ∑ j, V i j : ℝ) : ℂ) • x := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.IsHalfFilled, OAI.ContinuumCoulomb.HubbardGlobal.siteChargeOperator, OAI.ContinuumCoulomb.HubbardGlobal.chargePenaltyFock
def OAI.ContinuumCoulomb.HubbardGlobal.modeSite line 82
theorem OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_siteDiagonal line 85
theorem OAI.ContinuumCoulomb.HubbardGlobal.densityInteraction_site line 97
theorem OAI.ContinuumCoulomb.HubbardGlobal.densityInteraction_remove_self line 119
def OAI.ContinuumCoulomb.HubbardGlobal.siteCoulombCoefficient line 138
theorem OAI.ContinuumCoulomb.HubbardGlobal.densityInteraction_siteCoulomb line 141
theorem OAI.ContinuumCoulomb.HubbardGlobal.sum_siteCoulomb_self line 156
theorem OAI.ContinuumCoulomb.HubbardGlobal.directCoulomb_operator line 167
Source documentation
The actual diagonal Coulomb CAR tensor and compensating one-body matrix are the site-charge polynomial, before restricting particle number.
```
theorem directCoulomb_operator (m : ℕ) (U : ℝ)
    (V : Fin (m+1) → Fin (m+1) → ℝ) (hdiag : ∀ i, V i i = 0) :
    oneBodyOperator (fun a b => if a=b then
        -((∑ j, V (modeSite m a) j : ℝ):ℂ) else 0) +
      twoBodyOperator (fun a b c d => if a=c ∧ b=d then
        siteCoulombCoefficient U V (modeSite m a) (modeSite m b) else 0) =
      siteChargeOperator m U V := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator, OAI.ContinuumCoulomb.HubbardGlobal.modeSite, OAI.ContinuumCoulomb.HubbardGlobal.twoBodyOperator, OAI.ContinuumCoulomb.HubbardGlobal.siteCoulombCoefficient, OAI.ContinuumCoulomb.HubbardGlobal.siteChargeOperator