OAI/Analysis/LaughlinFock/ThreeRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Three Rows.

  1. theorem OAI.LaughlinFock.matrix_complete_column_sandwich line 16
  2. theorem OAI.LaughlinFock.sectorAverage_of_complete_spin line 31
  3. theorem OAI.LaughlinFock.threeSpinColumns_complete line 53
  4. theorem OAI.LaughlinFock.sectorAverage_three_kernel line 61
  5. theorem OAI.LaughlinFock.fockAverage_rowThreeBody line 95
  6. theorem OAI.LaughlinFock.spinRatio_eq_dimensions line 119
  7. theorem OAI.LaughlinFock.fockAverage_rowThreeBody_scaled line 128
  8. def OAI.LaughlinFock.averagedRowsFour line 153
  9. theorem OAI.LaughlinFock.fockAverage_rowsThreeBody line 160
  10. theorem OAI.LaughlinFock.averagedRows_positive line 181