OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardFermionSpectrum.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumCoulomb.HubbardGlobal.euclidean_real_inner line 12
2. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_real_inner line 19
3. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateRestriction_inclusion line 25
4. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFock_real_inner line 31
5. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFock_real_inner line 36
6. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFockRestriction_inclusion line 41
7. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockInclusion_norm_map line 45
8. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFockInclusion_norm_map line 49
9. theorem OAI.ContinuumCoulomb.HubbardGlobal.highOccupationIndex_ne_spin line 53
10. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction_highInclusion line 61
11. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFockRestriction_lowInclusion line 68
12. theorem OAI.ContinuumCoulomb.HubbardGlobal.low_high_inner_zero line 76
13. theorem OAI.ContinuumCoulomb.HubbardGlobal.low_high_norm_sq line 80
14. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_add_highProjection line 85
15. def OAI.ContinuumCoulomb.HubbardGlobal.assembleFock line 97
16. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockCoordinates_assemble line 101
17. theorem OAI.ContinuumCoulomb.HubbardGlobal.assembleFock_mass line 107
18. theorem OAI.ContinuumCoulomb.HubbardGlobal.assembleFock_halfFilled line 111
19. theorem OAI.ContinuumCoulomb.HubbardGlobal.assembleFock_decomposition line 130

    Source documentation

    Every vector in the full half-filled Fock sector has this low/high decomposition, not just vectors generated by a trial-state ansatz.

    theorem assembleFock_decomposition (m : ℕ) (x : Laughlin.Fock.Space (2 * m + 1))
        (hx : IsHalfFilled m x) :
        assembleFock m (lowFockRestriction m (fockCoordinates (2 * m + 1) x))
          (highFockRestriction m (fockCoordinates (2 * m + 1) x)) = x := by
    …

    Mentions: OAI.Laughlin.Fock.Space, OAI.ContinuumCoulomb.HubbardGlobal.IsHalfFilled, OAI.ContinuumCoulomb.HubbardGlobal.assembleFock, OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction, OAI.ContinuumCoulomb.HubbardGlobal.fockCoordinates, OAI.ContinuumCoulomb.HubbardGlobal.highFockRestriction

20. def OAI.ContinuumCoulomb.HubbardGlobal.chargePenaltyFock line 138
21. theorem OAI.ContinuumCoulomb.HubbardGlobal.chargePenaltyFock_spinEmbedding line 142
22. def OAI.ContinuumCoulomb.HubbardGlobal.actualChargePenalty line 152
23. theorem OAI.ContinuumCoulomb.HubbardGlobal.chargePenaltyFock_highInclusion line 156
24. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction_hopping_low line 174
25. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockHopping_real_symmetric line 187
26. def OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionForm line 198
27. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionForm_blocks line 205
28. def OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom line 250

    Source documentation

    The actual fermionic spectral bottom on all nonzero half-filled states, in the canonical occupation norm.

    def hubbardFermionBottom (m : ℕ) (U : ℝ) (V : Fin (m + 1) → Fin (m + 1) → ℝ)
        (left right : Edge → Fin (m + 1)) (t : Edge → ℝ) : ℝ :=
    …

29. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom_eq_blockBottom line 255
30. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom_Heisenberg line 285

    Source documentation

    The full fixed-particle fermion-to-Heisenberg energy comparison, with actual CAR hopping, long-range charge penalty and all spin states.

    theorem hubbardFermionBottom_Heisenberg (m : ℕ) (U R : ℝ)
        (V : Fin (m + 1) → Fin (m + 1) → ℝ)
        (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
        (hrow : ∀ i, ∑ j, |V i j| ≤ R) (hUR : R < U)
        (left right : Edge → Fin (m + 1)) (t J : Edge → ℝ)
        (hloop : ∀ e, left e ≠ right e)
        (hsimple : ∀ e f, e ≠ f →
          ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
        (hgap : ∀ e, U - V (left e) (right e) ≠ 0)
        (hcal : ∀ e, t e ^ 2 = J e * (U - V (left e) (right e)))
        {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon < 1 / 2)
        (ht : 4 * ∑ e, |t e| ≤ epsilon * (U - R)) :
    …