OAI/Analysis/LaughlinGap/FourComparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Four Comparison.

  1. def OAI.LaughlinGap.RealOccupation.fourHighestAverage line 16
  2. def OAI.LaughlinGap.RealOccupation.fourWeightCoefficient line 20
  3. def OAI.LaughlinGap.RealOccupation.fourWeightCoefficientStar line 23
  4. lemma OAI.LaughlinGap.RealOccupation.fourWeightCoefficient_tendsto line 26
  5. lemma OAI.LaughlinGap.RealOccupation.rowFour_cross_average line 35
  6. def OAI.LaughlinGap.RealOccupation.rowFourMatrix line 71
  7. lemma OAI.LaughlinGap.RealOccupation.rowFourMatrix_symmetric line 78
  8. lemma OAI.LaughlinGap.RealOccupation.rowFourMatrix_tendsto line 94
  9. lemma OAI.LaughlinGap.RealOccupation.rowFour_average line 106
  10. def OAI.LaughlinGap.RealOccupation.fourAverage line 142
  11. lemma OAI.LaughlinGap.RealOccupation.fourAverage_eq line 147
  12. lemma OAI.LaughlinGap.RealOccupation.rowFour_average_retained line 152
  13. def OAI.LaughlinGap.RealOccupation.fourCopyTarget line 167
  14. lemma OAI.LaughlinGap.RealOccupation.fourCopyTarget_symmetric line 170
  15. lemma OAI.LaughlinGap.RealOccupation.fourAverage_copyTarget line 174