OAI/Analysis/LaughlinGap/IrrepAveraging.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Irrep Averaging.

  1. lemma OAI.LaughlinGap.Spin.standardLadderSystem_casimir line 15
  2. theorem OAI.LaughlinGap.Spin.standardLadderMap_eq_zero line 22
  3. lemma OAI.LaughlinGap.Spin.ladderStep_pos line 39
  4. lemma OAI.LaughlinGap.Spin.weight_single line 44
  5. lemma OAI.LaughlinGap.Spin.lowering_single line 51
  6. theorem OAI.LaughlinGap.Spin.standardLadderMap_schur line 62
  7. theorem OAI.LaughlinGap.Spin.standardSpin_average line 104