OAI/Analysis/LaughlinFock/FiniteCoupling.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite Coupling.

  1. def OAI.LaughlinFock.highestWeight line 14
  2. def OAI.LaughlinFock.highestTotal line 17
  3. def OAI.LaughlinFock.highestCoefficient line 21
  4. theorem OAI.LaughlinFock.highestWeight_zero line 24
  5. theorem OAI.LaughlinFock.highestCoefficient_zero line 28
  6. theorem OAI.LaughlinFock.highestTotal_pos line 32
  7. theorem OAI.LaughlinFock.highestCoefficient_sq line 39
  8. theorem OAI.LaughlinFock.highestCoefficient_norm line 47
  9. theorem OAI.LaughlinFock.highestWeight_adjacent line 56
  10. theorem OAI.LaughlinFock.highestCoefficient_raising line 78
  11. theorem OAI.LaughlinFock.spin_complement_ratio_tendsto line 112
  12. theorem OAI.LaughlinFock.highestWeight_factorization line 124
  13. theorem OAI.LaughlinFock.highestWeight_scaled_tendsto line 142
  14. theorem OAI.LaughlinFock.highestTotal_scaled_tendsto line 160
  15. theorem OAI.LaughlinFock.highestCoefficient_tendsto line 181
  16. theorem OAI.LaughlinFock.highestCoefficient_tendsto_all line 201
  17. theorem OAI.LaughlinFock.root_affine_ratio_tendsto line 216
  18. def OAI.LaughlinFock.coupledCoefficient line 231
  19. theorem OAI.LaughlinFock.coupledCoefficient_zero line 242
  20. def OAI.LaughlinFock.oscillatorCoefficient line 254
  21. theorem OAI.LaughlinFock.oscillatorCoefficient_zero line 262
  22. theorem OAI.LaughlinFock.coupledCoefficient_tendsto line 276
  23. theorem OAI.LaughlinFock.highestWeight_mul_descFactorial line 340
  24. theorem OAI.LaughlinFock.highestCoefficient_ratio line 352
  25. theorem OAI.LaughlinFock.highestCoefficient_last line 385
  26. theorem OAI.LaughlinFock.highestCoefficient_penultimate line 393