OAI/Analysis/LaughlinGap/FastCoupling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fast Coupling.

  1. def OAI.LaughlinGap.Spin.chooseFast line 15
  2. lemma OAI.LaughlinGap.Spin.chooseFast_eq line 16
  3. def OAI.LaughlinGap.Spin.uFast line 19
  4. lemma OAI.LaughlinGap.Spin.uCoefficient_eq_fast line 23
  5. def OAI.LaughlinGap.RealOccupation.vFast line 32
  6. lemma OAI.LaughlinGap.RealOccupation.vCoefficient_eq_fast line 36
  7. def OAI.LaughlinGap.RealOccupation.RationalRow.fourSumEval line 39
  8. def OAI.LaughlinGap.RealOccupation.RationalRow.fourMatrixEval line 45
  9. lemma OAI.LaughlinGap.RealOccupation.RationalRow.fourMatrix_eq_eval line 49
  10. def OAI.LaughlinGap.RealOccupation.fourTermEval line 54
  11. lemma OAI.LaughlinGap.RealOccupation.fourTermCoefficient_eq_eval line 59
  12. lemma OAI.LaughlinGap.RealOccupation.fourColumn_eq_fiber line 63