OAI/Analysis/LaughlinGap/AuxiliaryComparison.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Auxiliary Comparison.

  1. abbrev OAI.LaughlinGap.RealOccupation.RowEntry line 16
  2. def OAI.LaughlinGap.RealOccupation.RowEntry.output line 19
  3. lemma OAI.LaughlinGap.RealOccupation.RowEntry.balance line 22
  4. structure OAI.LaughlinGap.RealOccupation.RowData line 26
  5. def OAI.LaughlinGap.RealOccupation.rowTriple line 31
  6. def OAI.LaughlinGap.RealOccupation.rowAnnihilator line 35
  7. def OAI.LaughlinGap.RealOccupation.rowThree line 39
  8. def OAI.LaughlinGap.RealOccupation.rowFour line 46
  9. lemma OAI.LaughlinGap.RealOccupation.rowSquare_split line 51
  10. lemma OAI.LaughlinGap.RealOccupation.rowSquare_average line 76
  11. def OAI.LaughlinGap.RealOccupation.threeWeightCoefficient line 89
  12. def OAI.LaughlinGap.RealOccupation.threeHighestAverage line 92
  13. lemma OAI.LaughlinGap.RealOccupation.sum_fin_extend line 97
  14. lemma OAI.LaughlinGap.RealOccupation.rowTriple_cross_average line 107
  15. def OAI.LaughlinGap.RealOccupation.rowTrace line 130
  16. def OAI.LaughlinGap.RealOccupation.rowThreeTrace line 139
  17. lemma OAI.LaughlinGap.RealOccupation.rowThree_average line 142