OAI/Analysis/LaughlinGap/PairDecomposition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Pair Decomposition.

  1. def OAI.LaughlinGap.Spin.tensorSwap line 18
  2. lemma OAI.LaughlinGap.Spin.highestCoefficient_last_equal_spin line 34
  3. theorem OAI.LaughlinGap.Spin.coupledTensor_swap line 41
  4. def OAI.LaughlinGap.Spin.orbitalPairCoefficient line 60
  5. lemma OAI.LaughlinGap.Spin.coupledTensor_antisymmetric line 63
  6. lemma OAI.LaughlinGap.Spin.coupledTensor_diag_zero line 68
  7. lemma OAI.LaughlinGap.Spin.orbitalPair_inner line 73
  8. theorem OAI.LaughlinGap.Spin.orbitalPair_orthonormal line 94
  9. theorem OAI.LaughlinGap.Spin.orbitalPairCoefficient_one line 114