OAI/Analysis/LaughlinFock/PairDecomposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Pair Decomposition.

  1. def OAI.LaughlinFock.fourCouplingMatrix line 13
  2. theorem OAI.LaughlinFock.fourCouplingMatrix_complete line 18
  3. theorem OAI.LaughlinFock.fourCouplingMatrix_gram line 36
  4. def OAI.LaughlinFock.fourCoupledWedgeMatrix line 66
  5. theorem OAI.LaughlinFock.fourCoupledWedgeMatrix_target line 71
  6. def OAI.LaughlinFock.retainedFourTarget line 83
  7. theorem OAI.LaughlinFock.retainedFourTarget_posSemidef line 88
  8. theorem OAI.LaughlinFock.discardedFourTarget_posSemidef line 98
  9. theorem OAI.LaughlinFock.discardedFourTarget_lift_posSemidef line 113
  10. theorem OAI.LaughlinFock.fourWedgeMatrix_swap line 120
  11. def OAI.LaughlinFock.fourCoupledAnnihilator line 126
  12. theorem OAI.LaughlinFock.fourCoupledAnnihilator_odd_zero line 133
  13. theorem OAI.LaughlinFock.fourWedgeMatrix_annihilator_column line 151
  14. theorem OAI.LaughlinFock.fourCoupledAnnihilator_eq_wedge line 160
  15. theorem OAI.LaughlinFock.retainedFourTarget_lift line 172