OAI/Analysis/LaughlinGap/FourTransfer.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Four Transfer.

  1. def OAI.LaughlinGap.RealOccupation.fourDimensionRatio line 17
  2. lemma OAI.LaughlinGap.RealOccupation.fourDimensionRatio_tendsto line 20
  3. lemma OAI.LaughlinGap.RealOccupation.fourDimensionRatio_eq line 36
  4. def OAI.LaughlinGap.RealOccupation.fourComparison line 44
  5. def OAI.LaughlinGap.RealOccupation.fourComparisonStar line 49
  6. lemma OAI.LaughlinGap.RealOccupation.fourComparison_symmetric line 54
  7. lemma OAI.LaughlinGap.RealOccupation.fourComparisonStar_symmetric line 66
  8. lemma OAI.LaughlinGap.RealOccupation.fourComparison_tendsto line 78
  9. def OAI.LaughlinGap.RealOccupation.localTripleP line 86
  10. def OAI.LaughlinGap.RealOccupation.localTripleJ line 88
  11. def OAI.LaughlinGap.RealOccupation.localTripleK line 90
  12. def OAI.LaughlinGap.RealOccupation.fourHighestRowsStar line 93
  13. def OAI.LaughlinGap.RealOccupation.fourLocalHighestStar line 97
  14. lemma OAI.LaughlinGap.RealOccupation.fourHighestRows_tendsto line 103
  15. def OAI.LaughlinGap.RealOccupation.FourCertificate line 107
  16. lemma OAI.LaughlinGap.RealOccupation.complexify_four_highest line 112
  17. lemma OAI.LaughlinGap.RealOccupation.lift_symmetric line 128
  18. lemma OAI.LaughlinGap.RealOccupation.posSemidef_of_complex_re line 135
  19. lemma OAI.LaughlinGap.RealOccupation.complexify_square_sum_inner line 144
  20. lemma OAI.LaughlinGap.RealOccupation.complexify_four_local_lift line 153
  21. theorem OAI.LaughlinGap.RealOccupation.four_local_transfer line 163