OAI/Analysis/LaughlinFock/FermionOperators.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Fermion Operators.

  1. def OAI.LaughlinFock.fermionSign line 12
  2. theorem OAI.LaughlinFock.annihilator_apply line 15
  3. theorem OAI.LaughlinFock.fermionSign_star line 19
  4. theorem OAI.LaughlinFock.fermionSign_mul_self line 22
  5. theorem OAI.LaughlinFock.sign_insert_lt line 28
  6. theorem OAI.LaughlinFock.sign_insert_not_lt line 33
  7. theorem OAI.LaughlinFock.sign_erase_lt line 37
  8. theorem OAI.LaughlinFock.sign_erase_not_lt line 45
  9. def OAI.LaughlinFock.creator line 54
  10. theorem OAI.LaughlinFock.mul_annihilator_apply line 58
  11. theorem OAI.LaughlinFock.mul_creator_apply line 69
  12. theorem OAI.LaughlinFock.creator_eq_adjoint line 80
  13. theorem OAI.LaughlinFock.annihilator_square line 94
  14. theorem OAI.LaughlinFock.annihilator_anticommute line 102
  15. theorem OAI.LaughlinFock.creator_mul_annihilator line 128
  16. theorem OAI.LaughlinFock.annihilator_mul_creator line 142
  17. theorem OAI.LaughlinFock.annihilator_creator_anticommute line 156
  18. theorem OAI.LaughlinFock.annihilator_adjoint_anticommute line 190
  19. theorem OAI.LaughlinFock.annihilator_norm_sq line 198
  20. theorem OAI.LaughlinFock.annihilator_contracts line 216
  21. theorem OAI.LaughlinFock.fourAnnihilator_norm_le_pair line 228
  22. def OAI.LaughlinFock.orbitalDelta line 238
  23. theorem OAI.LaughlinFock.delta_comm line 240
  24. theorem OAI.LaughlinFock.annihilator_creator_swap line 245
  25. theorem OAI.LaughlinFock.pair_normal_order line 252