OAI/Analysis/LaughlinGap/IntertwinerAveraging.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Intertwiner Averaging.

  1. def OAI.LaughlinGap.Spin.LadderMap.matrix line 17
  2. lemma OAI.LaughlinGap.Spin.LadderMap.matrix_mulVec line 21
  3. lemma OAI.LaughlinGap.Spin.LadderMap.matrix_lower line 25
  4. lemma OAI.LaughlinGap.Spin.LadderMap.matrix_raise line 31
  5. lemma OAI.LaughlinGap.Spin.LadderMap.transpose_matrix line 39
  6. def OAI.LaughlinGap.Spin.copyLift line 42
  7. lemma OAI.LaughlinGap.Spin.copyLift_commutator line 48
  8. lemma OAI.LaughlinGap.Spin.copyLift_commutator_transpose line 61
  9. theorem OAI.LaughlinGap.Spin.copyLift_average line 74
  10. lemma OAI.LaughlinGap.Spin.copyLift_rankOne line 83
  11. lemma OAI.LaughlinGap.Spin.trace_rankOne_mul line 90
  12. theorem OAI.LaughlinGap.Spin.distinct_copy_average line 94
  13. theorem OAI.LaughlinGap.Spin.equal_copy_average line 111