OAI/Analysis/LaughlinGap/PairSpin.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Pair Spin.

  1. theorem OAI.LaughlinGap.Spin.pairCoefficient_binomial line 15
  2. lemma OAI.LaughlinGap.Spin.sqrt_choose_lowering line 40
  3. def OAI.LaughlinGap.Spin.binomialPairTensor line 53
  4. lemma OAI.LaughlinGap.Spin.binomialPairTensor_swap line 58
  5. lemma OAI.LaughlinGap.Spin.binomialPairTensor_lower_first line 66
  6. theorem OAI.LaughlinGap.Spin.binomialPairTensor_lower line 86
  7. def OAI.LaughlinGap.Spin.physicalPairTensor line 106
  8. lemma OAI.LaughlinGap.Spin.physicalPairTensor_binomial line 109
  9. lemma OAI.LaughlinGap.Spin.pairNormalization_step line 117
  10. theorem OAI.LaughlinGap.Spin.physicalPairTensor_lower line 132
  11. lemma OAI.LaughlinGap.Spin.highestWeight_first_one line 139
  12. lemma OAI.LaughlinGap.Spin.highestNormalization_first line 146
  13. lemma OAI.LaughlinGap.Spin.sqrt_Q_over_sqrt_twoQ line 150
  14. theorem OAI.LaughlinGap.Spin.physicalPairTensor_zero line 156
  15. theorem OAI.LaughlinGap.Spin.physicalPairTensor_eq_coupled line 177