OAI/Analysis/LaughlinGap/ThreeGram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Three Gram.

  1. abbrev OAI.LaughlinGap.Spin.ThreeIndex line 14
  2. def OAI.LaughlinGap.Spin.cycleIndex line 16
  3. def OAI.LaughlinGap.Spin.cycleMap line 22
  4. lemma OAI.LaughlinGap.Spin.cycleMap_apply line 27
  5. lemma OAI.LaughlinGap.Spin.cycleMap_cube line 30
  6. lemma OAI.LaughlinGap.Spin.cycleMap_dot line 33
  7. lemma OAI.LaughlinGap.Spin.cycleMap_adjoint line 37
  8. def OAI.LaughlinGap.Spin.cyclicSum line 41
  9. lemma OAI.LaughlinGap.Spin.cyclicSum_apply line 44
  10. lemma OAI.LaughlinGap.Spin.cyclicSum_dot line 47
  11. lemma OAI.LaughlinGap.Spin.pairSpectatorInclusion_antisymmetric line 55
  12. lemma OAI.LaughlinGap.Spin.pairSpectatorInclusion_isometry line 62
  13. def OAI.LaughlinGap.Spin.orderedThreeWedge line 131
  14. lemma OAI.LaughlinGap.Spin.swap23Linear_adjoint line 136
  15. lemma OAI.LaughlinGap.Spin.cycleSquare_pairSpectatorInclusion line 146
  16. lemma OAI.LaughlinGap.Spin.cyclicSum_pair_dot line 154
  17. theorem OAI.LaughlinGap.Spin.orderedThreeWedge_dot line 173
  18. def OAI.LaughlinGap.Spin.orderedThreeGram line 184
  19. theorem OAI.LaughlinGap.Spin.orderedThreeGram_apply line 188
  20. theorem OAI.LaughlinGap.Spin.orderedThreeGram_eigenvalue line 197
  21. theorem OAI.LaughlinGap.Spin.orderedThreeGram_defect_expansion line 206
  22. lemma OAI.LaughlinGap.Spin.threeBodyGramCoefficient_zero line 227
  23. lemma OAI.LaughlinGap.Spin.threeBodyGramCoefficient_one line 230
  24. lemma OAI.LaughlinGap.Spin.threeBodyGramCoefficient_three line 241
  25. theorem OAI.LaughlinGap.Spin.orderedThreeWedge_null line 255