OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HalfFilledSector.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet_mem line 14
2. theorem OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet_card line 29
3. theorem OAI.ContinuumCoulomb.HubbardGlobal.occupationAt_spinOccupationSet line 33
4. theorem OAI.ContinuumCoulomb.HubbardGlobal.occupationAt_sum line 42

   Source documentation

   The sum of actual local particle counts is the cardinality of the occupied-mode set, including doubly occupied sites.

   theorem occupationAt_sum (m : ℕ) (A : Finset (Fin ((2 * m + 1) + 1))) :
       (∑ i, (occupationAt m A i : ℕ)) = A.card := by
   …

   Mentions: OAI.ContinuumCoulomb.HubbardGlobal.occupationAt

5. def OAI.ContinuumCoulomb.HubbardGlobal.occupationSpin line 59
6. theorem OAI.ContinuumCoulomb.HubbardGlobal.onePerSite_mem_iff line 63
7. theorem OAI.ContinuumCoulomb.HubbardGlobal.onePerSite_eq_spinOccupationSet line 73

   Source documentation

   Every one-electron-per-site occupation is a unique canonical spin occupation; there are no missing states in the low sector.

   theorem onePerSite_eq_spinOccupationSet (m : ℕ)
       (A : Finset (Fin ((2 * m + 1) + 1))) (hA : ∀ i, occupationAt m A i = 1) :
       A = spinOccupationSet m (occupationSpin m A) := by
   …

   Mentions: OAI.ContinuumCoulomb.HubbardGlobal.occupationAt, OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet, OAI.ContinuumCoulomb.HubbardGlobal.occupationSpin

8. abbrev OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledBasis line 80
9. abbrev OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledLowBasis line 83
10. abbrev OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledHighBasis line 86
11. def OAI.ContinuumCoulomb.HubbardGlobal.spinLowEquiv line 89
12. def OAI.ContinuumCoulomb.HubbardGlobal.halfFilledPartition line 105

    Source documentation

    An exact partition of the full fixed-particle basis, including all spin spectators in the charge-defect complement.

    def halfFilledPartition (m : ℕ) :
        SourceSpinBasis (m + 1) ⊕ HalfFilledHighBasis m ≃ HalfFilledBasis m :=
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledHighBasis, OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledBasis

13. theorem OAI.ContinuumCoulomb.HubbardGlobal.halfFilled_occupation_sum line 110