OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardExcitation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.HubbardGlobal.fockDiagonal line 15
2. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockDiagonal_basis line 18
3. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockDiagonal_coordinate line 23
4. def OAI.ContinuumCoulomb.HubbardGlobal.siteNumber line 39
5. def OAI.ContinuumCoulomb.HubbardGlobal.occupationAt line 42
6. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteNumber_basis line 46
7. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteNumber_eq_diagonal line 53
8. theorem OAI.ContinuumCoulomb.HubbardGlobal.numberEigen_coordinate_zero line 59
9. def OAI.ContinuumCoulomb.HubbardGlobal.occupationDiagonal line 72
10. theorem OAI.ContinuumCoulomb.HubbardGlobal.occupationDiagonal_eigen line 77

    Source documentation

    A joint local-number eigenvector has the corresponding value of every actual occupation-diagonal operator.

    theorem occupationDiagonal_eigen (m : ℕ) (f : (Fin (m + 1) → Fin 3) → ℂ)
        (o : Fin (m + 1) → Fin 3) (x : Space (2 * m + 1))
        (hx : ∀ i, siteNumber m i x = ((o i : ℕ) : ℂ) • x) :
        occupationDiagonal m f x = f o • x := by
    …

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.siteNumber, OAI.ContinuumCoulomb.HubbardGlobal.occupationDiagonal

11. def OAI.ContinuumCoulomb.HubbardGlobal.lowProjection line 96
12. def OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse line 99
13. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_eq_zero_of_numberEigen line 103
14. def OAI.ContinuumCoulomb.HubbardGlobal.chargeShift line 117
15. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteMode_delta_sum line 120
16. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteNumber_transfer_commutator line 128
17. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteNumber_transfer_eigen line 155

    Source documentation

    Hopping shifts the destination and source local particle numbers by exactly plus and minus one.

    theorem siteNumber_transfer_eigen (m : ℕ) (k i j : Fin (m + 1)) (σ τ : Fin 2)
        (x : Space (2 * m + 1)) (η : ℂ) (hx : siteNumber m k x = η • x) :
        siteNumber m k (transfer (siteMode m i σ) (siteMode m j τ) x) =
          (η + chargeShift k i j) • transfer (siteMode m i σ) (siteMode m j τ) x := by
    …

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.siteNumber, OAI.ContinuumCoulomb.HubbardGlobal.transfer, OAI.ContinuumCoulomb.HubbardGlobal.siteMode, OAI.ContinuumCoulomb.HubbardGlobal.chargeShift

18. theorem OAI.ContinuumCoulomb.HubbardGlobal.siteNumber_spinWedge line 169
19. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_spinWedge line 173
20. theorem OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse_transfer_spinWedge line 181

    Source documentation

    A genuine single hop creates the exact hole/double virtual charge sector. Its inverse denominator retains the direct repulsion V i j.

    theorem chargeInverse_transfer_spinWedge (m : ℕ) (U : ℝ)
        (V : Fin (m + 1) → Fin (m + 1) → ℝ)
        (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
        (s : SourceSpinBasis (m + 1)) (i j : Fin (m + 1)) (hij : i ≠ j) (σ τ : Fin 2) :
        chargeInverse m U V (transfer (siteMode m i σ) (siteMode m j τ) (spinWedge m s)) =
          (((U - V i j)⁻¹ : ℝ) : ℂ) •
            transfer (siteMode m i σ) (siteMode m j τ) (spinWedge m s) := by
    …

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

21. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_transfer_transfer_zero line 212

    Source documentation

    Two transfers cannot return to the singly occupied sector unless their oriented site changes are exact reverses.

    theorem lowProjection_transfer_transfer_zero (m : ℕ) (s : SourceSpinBasis (m + 1))
        (i j k l : Fin (m + 1)) (hij : i ≠ j) (hreverse : ¬(i = l ∧ j = k))
        (σ τ ρ υ : Fin 2) :
        lowProjection m
          (transfer (siteMode m i σ) (siteMode m j τ)
            (transfer (siteMode m k ρ) (siteMode m l υ) (spinWedge m s))) = 0 := by
    …

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

22. def OAI.ContinuumCoulomb.HubbardGlobal.siteHopping line 238
23. theorem OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse_hopping_spinWedge line 241
24. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_hopping_hopping_zero line 254

    Source documentation

    Different unordered edges have zero second-order low compression, with every spin channel and fermionic spectator retained.

    theorem lowProjection_hopping_hopping_zero (m : ℕ) (s : SourceSpinBasis (m + 1))
        (i j k l : Fin (m + 1)) (hij : i ≠ j)
        (hsame : ¬(i = k ∧ j = l)) (hreverse : ¬(i = l ∧ j = k)) :
        lowProjection m (siteHopping m i j (siteHopping m k l (spinWedge m s))) = 0 := by
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.lowProjection, OAI.ContinuumCoulomb.HubbardGlobal.siteHopping, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge

25. theorem OAI.ContinuumCoulomb.HubbardGlobal.hopping_inverse_hopping_spinWedge line 268

    Source documentation

    The same-edge inverse compression, with the exact Coulomb-modified denominator, acts as the expected Heisenberg superexchange numerator.

    theorem hopping_inverse_hopping_spinWedge (m : ℕ) (U : ℝ)
        (V : Fin (m + 1) → Fin (m + 1) → ℝ)
        (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
        (s : SourceSpinBasis (m + 1)) (i j : Fin (m + 1)) (hij : i ≠ j) :
        lowProjection m (siteHopping m i j (chargeInverse m U V (siteHopping m i j (spinWedge m s)))) =
          (((U - V i j)⁻¹ : ℝ) : ℂ) •
            ((2 : ℂ) • (spinWedge m s - spinWedge m (sourceSpinSwap i j s))) := by
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.lowProjection, OAI.ContinuumCoulomb.HubbardGlobal.siteHopping, OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge, OAI.ContinuumCoulomb.sourceSpinSwap

26. theorem OAI.ContinuumCoulomb.HubbardGlobal.cross_hopping_inverse_hopping_spinWedge line 281

    Source documentation

    All distinct-edge terms of the actual inverse compression vanish.

    theorem cross_hopping_inverse_hopping_spinWedge (m : ℕ) (U : ℝ)
        (V : Fin (m + 1) → Fin (m + 1) → ℝ)
        (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
        (s : SourceSpinBasis (m + 1)) (i j k l : Fin (m + 1)) (hij : i ≠ j) (hkl : k ≠ l)
        (hsame : ¬(i = k ∧ j = l)) (hreverse : ¬(i = l ∧ j = k)) :
        lowProjection m (siteHopping m i j (chargeInverse m U V (siteHopping m k l (spinWedge m s)))) =
          0 := by
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.lowProjection, OAI.ContinuumCoulomb.HubbardGlobal.siteHopping, OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge