OAI/Analysis/LaughlinFock/CreationRows.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Creation Rows.

  1. theorem OAI.LaughlinFock.creationRow_product line 13
  2. theorem OAI.LaughlinFock.square_sum_expansion line 31
  3. def OAI.LaughlinFock.auxiliaryRow line 51
  4. def OAI.LaughlinFock.rowTwoBody line 57
  5. def OAI.LaughlinFock.rowThreeBody line 61
  6. def OAI.LaughlinFock.rowFourBody line 74
  7. theorem OAI.LaughlinFock.auxiliaryRow_square line 82
  8. theorem OAI.LaughlinFock.rowTwoBody_mem line 95
  9. theorem OAI.LaughlinFock.orbitalPair_mem line 99
  10. theorem OAI.LaughlinFock.rowThreeBody_mem line 103
  11. theorem OAI.LaughlinFock.rowFourBody_mem line 123
  12. theorem OAI.LaughlinFock.auxiliaryRow_decomposition_posSemidef line 142
  13. def OAI.LaughlinFock.rowsComparison line 150
  14. theorem OAI.LaughlinFock.rowsComparison_posSemidef line 156
  15. theorem OAI.LaughlinFock.rowsComparison_decomposition line 162