OAI/Analysis/LaughlinGap/TensorSpin.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Tensor Spin.

  1. def OAI.LaughlinGap.Spin.ladderStep line 14
  2. lemma OAI.LaughlinGap.Spin.ladderStep_sq line 17
  3. def OAI.LaughlinGap.Spin.lowering line 22
  4. def OAI.LaughlinGap.Spin.raising line 31
  5. def OAI.LaughlinGap.Spin.weight line 40
  6. lemma OAI.LaughlinGap.Spin.lowering_zero line 45
  7. lemma OAI.LaughlinGap.Spin.lowering_succ line 46
  8. lemma OAI.LaughlinGap.Spin.raising_castSucc line 48
  9. lemma OAI.LaughlinGap.Spin.raising_last line 50
  10. lemma OAI.LaughlinGap.Spin.weight_apply line 52
  11. lemma OAI.LaughlinGap.Spin.raising_lowering_apply line 55
  12. lemma OAI.LaughlinGap.Spin.lowering_raising_apply line 64
  13. theorem OAI.LaughlinGap.Spin.raising_lowering_commutator line 74
  14. theorem OAI.LaughlinGap.Spin.weight_lowering_commutator line 80
  15. theorem OAI.LaughlinGap.Spin.lowering_raising_dot line 90
  16. structure OAI.LaughlinGap.Spin.LadderSystem line 100
  17. def OAI.LaughlinGap.Spin.standardLadderSystem line 108
  18. def OAI.LaughlinGap.Spin.LadderSystem.raw line 119
  19. lemma OAI.LaughlinGap.Spin.LadderSystem.raw_zero line 122
  20. lemma OAI.LaughlinGap.Spin.LadderSystem.raw_succ line 123
  21. lemma OAI.LaughlinGap.Spin.LadderSystem.weight_raw line 126
  22. lemma OAI.LaughlinGap.Spin.LadderSystem.raise_raw line 137
  23. theorem OAI.LaughlinGap.Spin.LadderSystem.raw_norm_sq line 148
  24. def OAI.LaughlinGap.Spin.LadderSystem.normalizationFactor line 170
  25. lemma OAI.LaughlinGap.Spin.LadderSystem.normalizationFactor_pos line 173
  26. lemma OAI.LaughlinGap.Spin.LadderSystem.normalizationFactor_succ line 178
  27. def OAI.LaughlinGap.Spin.LadderSystem.normalized line 186
  28. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_zero line 189
  29. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_succ line 192
  30. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_weight line 201
  31. theorem OAI.LaughlinGap.Spin.LadderSystem.normalized_norm_sq line 207
  32. def OAI.LaughlinGap.Spin.onFirstEnd line 223
  33. def OAI.LaughlinGap.Spin.onSecondEnd line 233
  34. lemma OAI.LaughlinGap.Spin.onFirstEnd_apply line 243
  35. lemma OAI.LaughlinGap.Spin.onSecondEnd_apply line 247
  36. lemma OAI.LaughlinGap.Spin.tensor_factor_commute line 251
  37. def OAI.LaughlinGap.Spin.LadderSystem.onFirst line 274
  38. def OAI.LaughlinGap.Spin.LadderSystem.onSecond line 291
  39. def OAI.LaughlinGap.Spin.LadderSystem.tensor line 307
  40. def OAI.LaughlinGap.Spin.tensorSpin line 338
  41. def OAI.LaughlinGap.Spin.highestTensor line 341
  42. def OAI.LaughlinGap.Spin.coupledTensor line 344
  43. lemma OAI.LaughlinGap.Spin.coupledTensor_zero line 347
  44. lemma OAI.LaughlinGap.Spin.tensorSpin_weight line 350
  45. lemma OAI.LaughlinGap.Spin.tensorSpin_lower line 357
  46. lemma OAI.LaughlinGap.Spin.tensorSpin_raise line 362
  47. lemma OAI.LaughlinGap.Spin.raising_apply_of_lt line 367
  48. lemma OAI.LaughlinGap.Spin.raising_apply_of_not_lt line 373
  49. theorem OAI.LaughlinGap.Spin.highestTensor_weight line 378
  50. theorem OAI.LaughlinGap.Spin.highestTensor_raise line 392
  51. theorem OAI.LaughlinGap.Spin.highestTensor_norm_sq line 424
  52. lemma OAI.LaughlinGap.Spin.firstLoweringCoefficient_succ line 463
  53. lemma OAI.LaughlinGap.Spin.secondLoweringCoefficient_succ line 471
  54. lemma OAI.LaughlinGap.Spin.secondLoweringCoefficient_last line 482
  55. theorem OAI.LaughlinGap.Spin.coupledTensor_succ line 489
  56. theorem OAI.LaughlinGap.Spin.coupledTensor_eq_normalized line 549
  57. theorem OAI.LaughlinGap.Spin.coupledTensor_norm_sq line 559
  58. theorem OAI.LaughlinGap.Spin.coupledTensor_weight line 565
  59. lemma OAI.LaughlinGap.Spin.LadderSystem.raise_adjoint line 575
  60. lemma OAI.LaughlinGap.Spin.LadderSystem.weight_eq line 579
  61. lemma OAI.LaughlinGap.Spin.LadderSystem.weight_adjoint line 584
  62. def OAI.LaughlinGap.Spin.LadderSystem.casimir line 589
  63. lemma OAI.LaughlinGap.Spin.LadderSystem.casimir_apply line 592
  64. lemma OAI.LaughlinGap.Spin.LadderSystem.casimir_adjoint line 596
  65. lemma OAI.LaughlinGap.Spin.LadderSystem.lower_raise_raw line 601
  66. lemma OAI.LaughlinGap.Spin.LadderSystem.casimir_raw line 612
  67. lemma OAI.LaughlinGap.Spin.LadderSystem.casimir_normalized line 620
  68. lemma OAI.LaughlinGap.Spin.dot_eq_zero_of_distinct_eigenvalues line 628
  69. theorem OAI.LaughlinGap.Spin.coupledTensor_casimir line 637
  70. theorem OAI.LaughlinGap.Spin.coupledTensor_orthogonal_same_spin line 644
  71. theorem OAI.LaughlinGap.Spin.coupledTensor_orthogonal_distinct_spin line 654
  72. abbrev OAI.LaughlinGap.Spin.CoupledIndex line 671
  73. def OAI.LaughlinGap.Spin.coupledFamily line 674
  74. theorem OAI.LaughlinGap.Spin.coupledFamily_orthonormal line 678
  75. theorem OAI.LaughlinGap.Spin.coupledIndex_card line 699
  76. def OAI.LaughlinGap.Spin.coupledBasis line 727
  77. theorem OAI.LaughlinGap.Spin.coupledBasis_apply line 737
  78. lemma OAI.LaughlinGap.Spin.LadderSystem.raw_top_succ line 744
  79. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_lower line 750
  80. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_lower_top line 758
  81. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_raise_zero line 763
  82. lemma OAI.LaughlinGap.Spin.LadderSystem.normalized_raise_succ line 766
  83. def OAI.LaughlinGap.Spin.LadderSystem.embedding line 782
  84. lemma OAI.LaughlinGap.Spin.LadderSystem.embedding_apply line 788
  85. theorem OAI.LaughlinGap.Spin.LadderSystem.embedding_lower line 791
  86. theorem OAI.LaughlinGap.Spin.LadderSystem.embedding_raise line 805
  87. theorem OAI.LaughlinGap.Spin.LadderSystem.embedding_weight line 819