OAI/Analysis/LaughlinGap/FourAllowance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Four Allowance.

  1. abbrev OAI.LaughlinGap.Spin.FourCoordinates line 15
  2. instance OAI.LaughlinGap.Spin.(instance at line 17) line 17
  3. def OAI.LaughlinGap.Spin.orbitalTripleFinite line 19
  4. lemma OAI.LaughlinGap.Spin.orbitalTripleFinite_injective line 25
  5. lemma OAI.LaughlinGap.Spin.sum_orbitalTriple line 35
  6. def OAI.LaughlinGap.Spin.fourHighestRows line 55
  7. lemma OAI.LaughlinGap.Spin.fourHighestRows_orthonormal line 58
  8. def OAI.LaughlinGap.RealOccupation.localFourCoordinates line 87
  9. lemma OAI.LaughlinGap.RealOccupation.fourAnnihilator_high_local line 92
  10. lemma OAI.LaughlinGap.RealOccupation.fourHighest_bessel line 107
  11. theorem OAI.LaughlinGap.RealOccupation.fourHighest_average_bessel line 121