OAI/Analysis/LaughlinGap/NormalOrder.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Normal Order.

  1. def OAI.LaughlinGap.Occupation.bodySpace line 14
  2. lemma OAI.LaughlinGap.Occupation.exteriorLift_single line 17
  3. lemma OAI.LaughlinGap.Occupation.word_rankOne_mem_bodySpace line 22
  4. lemma OAI.LaughlinGap.Occupation.triple_basic_eq_word line 41
  5. lemma OAI.LaughlinGap.Occupation.triple_rankOne_mem_bodySpace line 45
  6. lemma OAI.LaughlinGap.Occupation.middle_rankOne_mem_bodySpace line 61
  7. theorem OAI.LaughlinGap.Occupation.pairThreeTerm_mem_bodySpace line 68
  8. lemma OAI.LaughlinGap.Occupation.homogeneous_smul line 101
  9. lemma OAI.LaughlinGap.Occupation.homogeneous_sum line 106
  10. lemma OAI.LaughlinGap.Occupation.vacuum_homogeneous line 112
  11. lemma OAI.LaughlinGap.Occupation.creation_homogeneous line 117
  12. lemma OAI.LaughlinGap.Occupation.pairContraction_adjoint_homogeneous line 127
  13. def OAI.LaughlinGap.Occupation.sectorReadout line 137
  14. lemma OAI.LaughlinGap.Occupation.sectorReadout_apply line 142
  15. lemma OAI.LaughlinGap.Occupation.fullContraction_eq_exteriorContraction line 145
  16. lemma OAI.LaughlinGap.Occupation.reconstruct_pair_product line 162
  17. def OAI.LaughlinGap.Occupation.pairWedgeColumn line 176
  18. lemma OAI.LaughlinGap.Occupation.pairWedgeColumn_contraction line 179
  19. def OAI.LaughlinGap.Occupation.pairWedgeMatrix line 188
  20. theorem OAI.LaughlinGap.Occupation.pairFourTerm_eq_lift line 191
  21. theorem OAI.LaughlinGap.Occupation.pairFourTerm_positive line 207
  22. lemma OAI.LaughlinGap.Occupation.pairContraction_eq_pairAnnihilator line 217
  23. lemma OAI.LaughlinGap.Occupation.sectorInclusion_readout line 225
  24. lemma OAI.LaughlinGap.Occupation.sectorInclusion_adjoint line 232
  25. def OAI.LaughlinGap.Occupation.sectorExtract line 251
  26. lemma OAI.LaughlinGap.Occupation.sectorExtract_toEuclideanLin line 257
  27. theorem OAI.LaughlinGap.Occupation.sectorExtract_exteriorLift line 261
  28. lemma OAI.LaughlinGap.Occupation.exteriorLift_sectorExtract line 274
  29. lemma OAI.LaughlinGap.Occupation.sectorExtract_mul line 279
  30. lemma OAI.LaughlinGap.Occupation.sectorExtract_eq_zero line 290
  31. lemma OAI.LaughlinGap.Occupation.pairContraction_homogeneous line 299
  32. lemma OAI.LaughlinGap.Occupation.pairHamiltonian_homogeneous line 307
  33. lemma OAI.LaughlinGap.Occupation.numberOperator_apply line 314
  34. lemma OAI.LaughlinGap.Occupation.numberOperator_one line 324
  35. def OAI.LaughlinGap.Occupation.pairTripleOperator line 332
  36. lemma OAI.LaughlinGap.Occupation.pairTripleOperator_three line 337
  37. lemma OAI.LaughlinGap.Occupation.reconstruct_triple_pair line 346
  38. def OAI.LaughlinGap.Occupation.tripleWedgeColumn line 351
  39. lemma OAI.LaughlinGap.Occupation.tripleWedgeColumn_contraction line 355
  40. def OAI.LaughlinGap.Occupation.tripleWedgeMatrix line 363
  41. lemma OAI.LaughlinGap.Occupation.pairTripleOperator_eq_lift line 366
  42. lemma OAI.LaughlinGap.Occupation.pairHamiltonian_sector_three line 387
  43. theorem OAI.LaughlinGap.Occupation.pairThreeTerm_eq_lift line 400
  44. theorem OAI.LaughlinGap.Occupation.normal_ordered_square line 423
  45. lemma OAI.LaughlinGap.Occupation.sum_increasing_pairs line 438
  46. lemma OAI.LaughlinGap.Occupation.sphericalExteriorPairCoefficient_eq_tensor line 459
  47. def OAI.LaughlinGap.Occupation.physicalPairForms line 467
  48. lemma OAI.LaughlinGap.Occupation.physicalPair_contraction line 470
  49. theorem OAI.LaughlinGap.Occupation.physicalPairForms_orthonormal line 475
  50. def OAI.LaughlinGap.Occupation.physicalOccupationHamiltonian line 498
  51. theorem OAI.LaughlinGap.Occupation.physical_normal_ordered_square line 501
  52. lemma OAI.LaughlinGap.Occupation.pairContraction_eq_zero_of_degree_lt line 517
  53. lemma OAI.LaughlinGap.Occupation.pairHamiltonian_preserves_degree line 526
  54. theorem OAI.LaughlinGap.Occupation.physicalOccupationHamiltonian_positive line 538
  55. theorem OAI.LaughlinGap.Occupation.physicalOccupationHamiltonian_inner line 544
  56. lemma OAI.LaughlinGap.Occupation.numberOperator_homogeneous line 561
  57. lemma OAI.LaughlinGap.Occupation.sum_annihilation_norm_sq line 570
  58. def OAI.LaughlinGap.Occupation.rawReadout line 581
  59. lemma OAI.LaughlinGap.Occupation.rawReadout_apply line 586
  60. lemma OAI.LaughlinGap.Occupation.rawReadout_succ line 589
  61. theorem OAI.LaughlinGap.Occupation.rawReadout_norm_sq line 593
  62. def OAI.LaughlinGap.Occupation.normalizedReadout line 614
  63. lemma OAI.LaughlinGap.Occupation.normalizedReadout_apply line 618
  64. lemma OAI.LaughlinGap.Occupation.normalizedReadout_norm_sq line 622