OAI/Analysis/LaughlinFock/FockRotations.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Fock Rotations.

  1. def OAI.LaughlinFock.sectorOneBodyLinear line 12
  2. inductive OAI.LaughlinFock.FockRotationIndex line 21
  3. abbrev OAI.LaughlinFock.FockRotationSpace line 29
  4. instance OAI.LaughlinFock.(instance at line 34) line 34
  5. instance OAI.LaughlinFock.(instance at line 36) line 36
  6. def OAI.LaughlinFock.fockRotationGenerator line 40
  7. theorem OAI.LaughlinFock.fockRotationGenerator_skew line 46
  8. def OAI.LaughlinFock.fockAverage line 60
  9. def OAI.LaughlinFock.sectorAverage line 64
  10. theorem OAI.LaughlinFock.fockAverage_exteriorLift line 70
  11. theorem OAI.LaughlinFock.fockAverage_posSemidef line 77
  12. theorem OAI.LaughlinFock.sectorAverage_posSemidef line 81
  13. theorem OAI.LaughlinFock.spinRotationAverage line 88
  14. def OAI.LaughlinFock.congruenceLinear line 99
  15. theorem OAI.LaughlinFock.congruenceLinear_commutator line 107
  16. theorem OAI.LaughlinFock.sectorAverage_spin_sandwich line 122
  17. theorem OAI.LaughlinFock.fockAverage_spin_sandwich line 139