OAI/Analysis/LaughlinFock/Covariance.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Covariance.

  1. def OAI.LaughlinFock.oneBodyLift line 13
  2. theorem OAI.LaughlinFock.oneBodyLift_add line 16
  3. theorem OAI.LaughlinFock.oneBodyLift_smul line 20
  4. def OAI.LaughlinFock.oneBodyLiftLinear line 24
  5. theorem OAI.LaughlinFock.oneBodyLift_adjoint line 30
  6. theorem OAI.LaughlinFock.oneBodyLift_hermitian line 37
  7. theorem OAI.LaughlinFock.annihilator_oneBody_unit_commutator line 43
  8. theorem OAI.LaughlinFock.annihilator_oneBody_commutator line 61
  9. theorem OAI.LaughlinFock.oneBody_creator_commutator line 74
  10. theorem OAI.LaughlinFock.matrix_commutator_mul line 84
  11. theorem OAI.LaughlinFock.oneBody_annihilator_commutator_mem line 91
  12. theorem OAI.LaughlinFock.oneBody_annihilatorList_commutator_mem line 101
  13. theorem OAI.LaughlinFock.oneBody_annihilationSpace_commutator_mem line 116
  14. theorem OAI.LaughlinFock.oneBodyLift_vacuum_row line 130
  15. theorem OAI.LaughlinFock.oneBodyLift_vacuum_column line 136
  16. theorem OAI.LaughlinFock.oneBodyLift_entry_eq_zero line 143
  17. def OAI.LaughlinFock.sectorOneBody line 161
  18. theorem OAI.LaughlinFock.sectorOneBody_adjoint line 165
  19. theorem OAI.LaughlinFock.oneBody_basis_commutator line 172
  20. theorem OAI.LaughlinFock.oneBody_basisCreator_commutator line 191
  21. theorem OAI.LaughlinFock.oneBody_wedgeAnnihilator_commutator line 208
  22. theorem OAI.LaughlinFock.oneBody_exteriorLift_commutator line 223
  23. theorem OAI.LaughlinFock.oneBodyLift_commutator line 275