OAI/Analysis/LaughlinGap/Four.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Four.

  1. lemma OAI.LaughlinGap.Spin.tensorProjection_positive line 15
  2. lemma OAI.LaughlinGap.Spin.sum_tensorProjection line 23
  3. lemma OAI.LaughlinGap.RealOccupation.Covariant.average_highest line 40
  4. def OAI.LaughlinGap.RealOccupation.physicalPairPair line 55
  5. lemma OAI.LaughlinGap.RealOccupation.physicalPairPair_covariant line 59
  6. lemma OAI.LaughlinGap.RealOccupation.fourAnnihilator_first line 63
  7. lemma OAI.LaughlinGap.RealOccupation.lift_physicalPairPair_one line 91
  8. theorem OAI.LaughlinGap.RealOccupation.fourTarget_retained line 106