OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardOccupation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.HubbardGlobal.fockBasis line 15
2. theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_unoccupied_wedge line 18
3. theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_unoccupied_basis line 37
4. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockBasis_singleton line 52
5. theorem OAI.ContinuumCoulomb.HubbardGlobal.create_occupied_basis line 65
6. theorem OAI.ContinuumCoulomb.HubbardGlobal.number_basis line 77

   Source documentation

   Each actual number operator is diagonal in the full occupation basis, including every spectator mode.

   theorem number_basis (i : Fin (Q + 1)) (A : Finset (Fin (Q + 1))) :
       number i (fockBasis Q A) = if i ∈ A then fockBasis Q A else 0 := by
   …

   Mentions: OAI.ContinuumCoulomb.HubbardGlobal.number, OAI.ContinuumCoulomb.HubbardGlobal.fockBasis