OAI/Analysis/LaughlinGap/ThreeBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Three Bounds.

  1. lemma OAI.LaughlinGap.RealOccupation.combination_one_bessel line 18
  2. lemma OAI.LaughlinGap.RealOccupation.highestCombination_range line 29
  3. def OAI.LaughlinGap.RealOccupation.threeSpinLift line 60
  4. lemma OAI.LaughlinGap.RealOccupation.threeSpinLift_positive line 63
  5. lemma OAI.LaughlinGap.RealOccupation.threeSpinLift_average_highest line 72
  6. lemma OAI.LaughlinGap.RealOccupation.average_mono line 88
  7. lemma OAI.LaughlinGap.RealOccupation.threeSpinLift_le line 94
  8. lemma OAI.LaughlinGap.RealOccupation.physicalHamiltonian_positive line 138
  9. lemma OAI.LaughlinGap.RealOccupation.threeTailTerm_le line 141
  10. def OAI.LaughlinGap.RealOccupation.threeTailLift line 171
  11. theorem OAI.LaughlinGap.RealOccupation.threeTailLift_le line 175