OAI/Analysis/LaughlinFock/RowTraces.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Row Traces.

  1. def OAI.LaughlinFock.rowThreePrewedge line 14
  2. theorem OAI.LaughlinFock.exteriorLift_single_congruence line 24
  3. theorem OAI.LaughlinFock.rowThreePrewedge_lift line 34
  4. theorem OAI.LaughlinFock.single_bilinear line 64
  5. theorem OAI.LaughlinFock.rowThreePrewedge_bilinear line 71
  6. abbrev OAI.LaughlinFock.RowEntry line 95
  7. def OAI.LaughlinFock.rowP line 97
  8. def OAI.LaughlinFock.rowJ line 98
  9. def OAI.LaughlinFock.rowI line 99
  10. theorem OAI.LaughlinFock.rowEntry_bounds line 101
  11. theorem OAI.LaughlinFock.rowI_eq_iff line 109
  12. def OAI.LaughlinFock.rowFourLevel line 116
  13. theorem OAI.LaughlinFock.rowFourLevel_symm line 118
  14. theorem OAI.LaughlinFock.rowFourLevel_le line 125
  15. def OAI.LaughlinFock.sphericalThreeCoefficient line 132
  16. def OAI.LaughlinFock.planarThreeCoefficient line 136
  17. theorem OAI.LaughlinFock.sphericalThreeCoefficient_tendsto line 140
  18. def OAI.LaughlinFock.rowThreeTrace line 150
  19. def OAI.LaughlinFock.planarRowThreeTrace line 158
  20. theorem OAI.LaughlinFock.rowThreeTrace_tendsto line 167
  21. def OAI.LaughlinFock.rowFourTrace line 187
  22. def OAI.LaughlinFock.planarRowFourTrace line 193
  23. theorem OAI.LaughlinFock.rowFourTrace_tendsto line 200
  24. theorem OAI.LaughlinFock.rowFourTrace_symmetric line 215
  25. theorem OAI.LaughlinFock.planarRowFourTrace_symmetric line 229