OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardSpin.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.HubbardGlobal.wedgeModes line 17
2. theorem OAI.ContinuumCoulomb.HubbardGlobal.wedgeModes_succ line 20
3. theorem OAI.ContinuumCoulomb.HubbardGlobal.wedgeModes_replace_zero line 24
4. theorem OAI.ContinuumCoulomb.HubbardGlobal.wedgeModes_replace_succ line 30
5. theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_create line 38

   Source documentation

   Even fermion bilinears pass a spectator creator without a sign.

   theorem transfer_create (i j k : Fin (Q + 1)) :
       transfer i j * create k =
         delta j k • create i + create k * transfer i j := by
   …

   Mentions: OAI.ContinuumCoulomb.HubbardGlobal.transfer

6. theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_wedgeModes line 51

   Source documentation

   The action of a bilinear on an arbitrary wedge is the sum of its one-particle replacements, with all CAR signs derived.

   theorem transfer_wedgeModes (i j : Fin (Q + 1)) (n : ℕ)
       (v : Fin n → Fin (Q + 1)) :
       transfer i j (wedgeModes n v) =
         ∑ k, delta j (v k) • wedgeModes n (fun a => if a = k then i else v a) := by
   …

   Mentions: OAI.ContinuumCoulomb.HubbardGlobal.transfer, OAI.ContinuumCoulomb.HubbardGlobal.wedgeModes

7. def OAI.ContinuumCoulomb.HubbardGlobal.siteModes line 70
8. def OAI.ContinuumCoulomb.HubbardGlobal.siteMode line 73
9. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteMode_eq_iff line 76
10. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteMode_ne_of_ne line 81
11. def OAI.ContinuumCoulomb.HubbardGlobal.spinWedge line 85
12. theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_spinWedge line 90

    Source documentation

    Local spin flips act with coefficient one on the ordered wedge; spectator parities cancel because the operator is an even bilinear.

    theorem transfer_spinWedge (m : ℕ) (s : Fin (m + 1) → Fin 2)
        (i : Fin (m + 1)) (σ τ : Fin 2) :
        transfer (siteMode m i σ) (siteMode m i τ) (spinWedge m s) =
          if s i = τ then spinWedge m (Function.update s i σ) else 0 := by
    …

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.transfer, OAI.ContinuumCoulomb.HubbardGlobal.siteMode, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge

13. theorem OAI.ContinuumCoulomb.HubbardGlobal.sourceSpinSwap_eq_updates line 125
14. theorem OAI.ContinuumCoulomb.HubbardGlobal.number_spinWedge line 137
15. theorem OAI.ContinuumCoulomb.HubbardGlobal.local_number_spinWedge line 146
16. theorem OAI.ContinuumCoulomb.HubbardGlobal.transfers_spinWedge line 153
17. theorem OAI.ContinuumCoulomb.HubbardGlobal.spinSwap_eq_sum line 166
18. theorem OAI.ContinuumCoulomb.HubbardGlobal.spinSwap_spinWedge line 181

    Source documentation

    The fermionic exchange is exactly the source coordinate swap, including its sign and every spectator spin.

    theorem spinSwap_spinWedge (m : ℕ) (s : Fin (m + 1) → Fin 2)
        (i j : Fin (m + 1)) (hij : i ≠ j) :
        spinSwap (siteMode m i 0) (siteMode m i 1) (siteMode m j 0) (siteMode m j 1)
            (spinWedge m s) = spinWedge m (sourceSpinSwap i j s) := by
    …

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.spinSwap, OAI.ContinuumCoulomb.HubbardGlobal.siteMode, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge, OAI.ContinuumCoulomb.sourceSpinSwap

19. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteHeisenberg_spinWedge line 203
20. theorem OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping_sq_spinWedge line 213

    Source documentation

    The genuine many-mode hopping square gives the Heisenberg superexchange numerator on every spin configuration.

    theorem twoSiteHopping_sq_spinWedge (m : ℕ) (s : Fin (m + 1) → Fin 2)
        (i j : Fin (m + 1)) (hij : i ≠ j) :
        (twoSiteHopping (siteMode m i 0) (siteMode m i 1) (siteMode m j 0) (siteMode m j 1) *
          twoSiteHopping (siteMode m i 0) (siteMode m i 1) (siteMode m j 0) (siteMode m j 1))
            (spinWedge m s) =
          (2 : ℂ) • (spinWedge m s - spinWedge m (sourceSpinSwap i j s)) := by
    …

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping, OAI.ContinuumCoulomb.HubbardGlobal.siteMode, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge, OAI.ContinuumCoulomb.sourceSpinSwap