OAI/Analysis/LaughlinFock/NormalOrdering.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Normal Ordering.

  1. def OAI.LaughlinFock.annihilatorList line 22
  2. theorem OAI.LaughlinFock.annihilatorList_nil line 26
  3. theorem OAI.LaughlinFock.annihilatorList_cons line 28
  4. def OAI.LaughlinFock.basisAnnihilator line 32
  5. theorem OAI.LaughlinFock.annihilatorList_entry_eq_zero line 35
  6. theorem OAI.LaughlinFock.basisAnnihilator_entry_eq_zero line 51
  7. theorem OAI.LaughlinFock.annihilatorList_vacuum line 56
  8. theorem OAI.LaughlinFock.basisAnnihilator_vacuum line 90
  9. theorem OAI.LaughlinFock.basisAnnihilator_same_sector line 95
  10. def OAI.LaughlinFock.wedgeAnnihilator line 109
  11. def OAI.LaughlinFock.exteriorLift line 113
  12. theorem OAI.LaughlinFock.exteriorLift_posSemidef line 119
  13. theorem OAI.LaughlinFock.exteriorLift_rankOne line 129
  14. theorem OAI.LaughlinFock.basisAnnihilator_gram_same_sector line 143
  15. theorem OAI.LaughlinFock.exteriorLift_same_sector line 156
  16. theorem OAI.LaughlinFock.exteriorLift_below_sector line 168
  17. theorem OAI.LaughlinFock.annihilator_swap line 191
  18. theorem OAI.LaughlinFock.annihilatorList_append line 195
  19. theorem OAI.LaughlinFock.annihilatorList_perm line 203
  20. theorem OAI.LaughlinFock.annihilatorList_mul_of_mem line 219
  21. theorem OAI.LaughlinFock.annihilatorList_eq_zero_of_not_nodup line 230
  22. theorem OAI.LaughlinFock.annihilatorList_expansion line 243
  23. theorem OAI.LaughlinFock.exteriorLift_congruence line 269
  24. theorem OAI.LaughlinFock.exteriorLift_of_gram_certificate line 283
  25. def OAI.LaughlinFock.AnnihilationSpace line 295
  26. theorem OAI.LaughlinFock.basisAnnihilator_mem line 298
  27. theorem OAI.LaughlinFock.annihilatorList_mem line 302
  28. theorem OAI.LaughlinFock.annihilationSpace_normal_form line 307
  29. theorem OAI.LaughlinFock.annihilationSpace_ext line 329
  30. theorem OAI.LaughlinFock.annihilationSpace_mul line 337
  31. theorem OAI.LaughlinFock.annihilator_mem line 353
  32. theorem OAI.LaughlinFock.coefficientPairAnnihilator_mem line 358
  33. theorem OAI.LaughlinFock.pairAnnihilator_mem line 371
  34. theorem OAI.LaughlinFock.limitPairAnnihilator_mem line 375
  35. theorem OAI.LaughlinFock.localPairAnnihilator_mem line 379
  36. def OAI.LaughlinFock.annihilatorVector line 385
  37. theorem OAI.LaughlinFock.wedgeAnnihilator_mem line 388
  38. theorem OAI.LaughlinFock.wedgeAnnihilator_annihilatorVector line 393
  39. theorem OAI.LaughlinFock.exteriorLift_annihilator_product line 401
  40. def OAI.LaughlinFock.exteriorLiftLinear line 409
  41. theorem OAI.LaughlinFock.exteriorLift_add line 418
  42. theorem OAI.LaughlinFock.exteriorLift_sub line 423
  43. theorem OAI.LaughlinFock.exteriorLift_sum line 428
  44. def OAI.LaughlinFock.BodySpace line 435
  45. theorem OAI.LaughlinFock.bodySpace_product line 438
  46. theorem OAI.LaughlinFock.bodySpace_reconstruct line 443
  47. theorem OAI.LaughlinFock.bodySpace_below_sector line 449
  48. theorem OAI.LaughlinFock.bodySpace_two_decomposition line 458
  49. theorem OAI.LaughlinFock.annihilator_commutes_pair line 472
  50. theorem OAI.LaughlinFock.annihilator_commutes_coefficientPair line 479
  51. theorem OAI.LaughlinFock.coefficientPairs_commute line 494
  52. theorem OAI.LaughlinFock.pairAnnihilators_commute line 512
  53. theorem OAI.LaughlinFock.annihilationSpace_two_induction line 519
  54. theorem OAI.LaughlinFock.pair_monomial_commutator_bodies line 538
  55. theorem OAI.LaughlinFock.pair_commutator_bodies line 590
  56. def OAI.LaughlinFock.fourBodyTerm line 631
  57. theorem OAI.LaughlinFock.fourBodyTerm_posSemidef line 636
  58. theorem OAI.LaughlinFock.hamiltonian_mem_bodySpace line 643
  59. theorem OAI.LaughlinFock.fourBodyTerm_mem_bodySpace line 647
  60. theorem OAI.LaughlinFock.square_remainder_commutators line 655
  61. theorem OAI.LaughlinFock.square_remainder_mem_bodies line 679
  62. theorem OAI.LaughlinFock.normal_square_of_pair_projection line 691
  63. abbrev OAI.LaughlinFock.IncreasingPair line 728
  64. theorem OAI.LaughlinFock.sort_pair line 730
  65. def OAI.LaughlinFock.increasingPairSector line 737
  66. theorem OAI.LaughlinFock.increasingPairSector_injective line 740
  67. theorem OAI.LaughlinFock.increasingPairSector_surjective line 747
  68. def OAI.LaughlinFock.increasingPairEquiv line 762
  69. theorem OAI.LaughlinFock.increasingPairEquiv_apply line 766
  70. theorem OAI.LaughlinFock.increasingPair_sum line 769
  71. theorem OAI.LaughlinFock.basisAnnihilator_pair line 778
  72. theorem OAI.LaughlinFock.coefficientPair_basis_expansion line 783
  73. theorem OAI.LaughlinFock.coefficientPair_vacuum line 798
  74. def OAI.LaughlinFock.pairVector line 809
  75. theorem OAI.LaughlinFock.pairVector_increasing line 812
  76. theorem OAI.LaughlinFock.pairVector_orthonormal line 820
  77. abbrev OAI.LaughlinFock.PairLabel line 845
  78. def OAI.LaughlinFock.pairWedgeMatrix line 848
  79. theorem OAI.LaughlinFock.pairWedgeMatrix_gram line 851
  80. theorem OAI.LaughlinFock.hamiltonian_exteriorLift line 859
  81. theorem OAI.LaughlinFock.sectorHamiltonian_two line 869
  82. theorem OAI.LaughlinFock.sectorHamiltonian_two_projection line 876
  83. theorem OAI.LaughlinFock.normal_square line 884
  84. def OAI.LaughlinFock.threeWedgeMatrix line 891
  85. def OAI.LaughlinFock.fourWedgeMatrix line 897
  86. theorem OAI.LaughlinFock.basisAnnihilator_singleton line 902
  87. theorem OAI.LaughlinFock.annihilator_vacuum line 907
  88. theorem OAI.LaughlinFock.annihilator_mul_vacuum line 911
  89. def OAI.LaughlinFock.singletonSectorEquiv line 917
  90. theorem OAI.LaughlinFock.sum_singleton_support line 923
  91. theorem OAI.LaughlinFock.threeWedgeMatrix_apply line 936
  92. theorem OAI.LaughlinFock.sectorHamiltonian_three line 943
  93. theorem OAI.LaughlinFock.fourBodyTerm_exteriorLift line 961
  94. theorem OAI.LaughlinFock.normal_ordered_square line 982