OAI/Analysis/LaughlinGap/IntertwiningSpin.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Intertwining Spin.

  1. def OAI.LaughlinGap.Spin.transposeMap line 14
  2. lemma OAI.LaughlinGap.Spin.transposeMap_adjoint line 22
  3. lemma OAI.LaughlinGap.Spin.eq_of_dotProduct_eq line 37
  4. structure OAI.LaughlinGap.Spin.LadderMap line 43
  5. lemma OAI.LaughlinGap.Spin.LadderMap.weight line 52
  6. lemma OAI.LaughlinGap.Spin.LadderMap.casimir line 56
  7. def OAI.LaughlinGap.Spin.LadderMap.comp line 60
  8. def OAI.LaughlinGap.Spin.LadderMap.transpose line 65
  9. lemma OAI.LaughlinGap.Spin.LadderMap.raw line 78
  10. lemma OAI.LaughlinGap.Spin.LadderMap.normalized line 84
  11. def OAI.LaughlinGap.Spin.LadderSystem.embeddingMap line 90
  12. def OAI.LaughlinGap.Spin.coupledEmbedding line 98
  13. lemma OAI.LaughlinGap.Spin.coupledEmbedding_apply line 102
  14. theorem OAI.LaughlinGap.Spin.coupledTensor_expansion line 109
  15. lemma OAI.LaughlinGap.Spin.spinCasimir_injective line 122
  16. theorem OAI.LaughlinGap.Spin.coupledHighest_eigenline line 132
  17. lemma OAI.LaughlinGap.Spin.LadderSystem.raw_smul line 176
  18. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_smul line 182
  19. theorem OAI.LaughlinGap.Spin.tensorSpin_schur line 187