OAI/Analysis/LaughlinGap/RealOccupation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Real Occupation.

  1. def OAI.LaughlinGap.RealOccupation.complexify line 17
  2. lemma OAI.LaughlinGap.RealOccupation.complexify_injective line 34
  3. lemma OAI.LaughlinGap.RealOccupation.complexify_transpose line 42
  4. lemma OAI.LaughlinGap.RealOccupation.complexify_positive line 50
  5. abbrev OAI.LaughlinGap.RealOccupation.FockMatrix line 63
  6. def OAI.LaughlinGap.RealOccupation.annihilation line 65
  7. def OAI.LaughlinGap.RealOccupation.creation line 69
  8. theorem OAI.LaughlinGap.RealOccupation.complexify_annihilation line 72
  9. theorem OAI.LaughlinGap.RealOccupation.complexify_creation line 83
  10. lemma OAI.LaughlinGap.RealOccupation.creation_transpose line 88
  11. lemma OAI.LaughlinGap.RealOccupation.annihilation_creation line 91
  12. lemma OAI.LaughlinGap.RealOccupation.annihilation_anticommute line 99
  13. lemma OAI.LaughlinGap.RealOccupation.creation_anticommute line 105
  14. def OAI.LaughlinGap.RealOccupation.secondQuantization line 110
  15. lemma OAI.LaughlinGap.RealOccupation.secondQuantization_transpose line 113
  16. lemma OAI.LaughlinGap.RealOccupation.elementary_commutator_annihilation line 119
  17. lemma OAI.LaughlinGap.RealOccupation.commutator_annihilation line 132
  18. lemma OAI.LaughlinGap.RealOccupation.commutator_mul line 146