OAI/Analysis/LaughlinFock/FastWedge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Fast Wedge.

  1. def OAI.LaughlinFock.occupationWeight line 12
  2. def OAI.LaughlinFock.fastHighestTerm line 15
  3. def OAI.LaughlinFock.fastHighestEntry line 22
  4. theorem OAI.LaughlinFock.fourHighestShell_sum line 25
  5. theorem OAI.LaughlinFock.highest_pair_weight_sum line 34
  6. theorem OAI.LaughlinFock.rationalHighestEntry_expand line 59
  7. theorem OAI.LaughlinFock.fastHighestTerm_support line 107
  8. theorem OAI.LaughlinFock.rationalHighestEntry_fast line 117
  9. theorem OAI.LaughlinFock.fastHighestTerm_weight line 141
  10. theorem OAI.LaughlinFock.rationalHighestEntry_weight line 160
  11. def OAI.LaughlinFock.highestFourOccupations line 176
  12. def OAI.LaughlinFock.fastFourGram line 180
  13. theorem OAI.LaughlinFock.rationalFourGram_fast line 185