OAI/Analysis/LaughlinGap/SpinAveraging.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Spin Averaging.

  1. def OAI.LaughlinGap.Spin.loweringMatrix line 16
  2. lemma OAI.LaughlinGap.Spin.loweringMatrix_transpose line 19
  3. def OAI.LaughlinGap.Spin.commutantLadderMap line 25
  4. lemma OAI.LaughlinGap.Spin.ladderMap_matrix_mem line 42
  5. lemma OAI.LaughlinGap.Spin.toMatrix_transposeMap line 61
  6. def OAI.LaughlinGap.Spin.tensorProjection line 73
  7. lemma OAI.LaughlinGap.Spin.tensorProjection_mem line 77
  8. lemma OAI.LaughlinGap.Spin.coupledEmbedding_entry line 81
  9. lemma OAI.LaughlinGap.Spin.tensorProjection_eq line 87
  10. lemma OAI.LaughlinGap.Spin.coupledTensor_dot line 96
  11. lemma OAI.LaughlinGap.Spin.tensorProjection_mulVec line 102
  12. lemma OAI.LaughlinGap.Spin.trace_mul_rankOne line 125
  13. theorem OAI.LaughlinGap.Spin.tensorSpin_average line 129