OAI/Analysis/LaughlinGap/ThreeComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Three Comparison.

  1. def OAI.LaughlinGap.RealOccupation.threeWeightCoefficientStar line 17
  2. lemma OAI.LaughlinGap.RealOccupation.threeWeightCoefficient_tendsto line 21
  3. lemma OAI.LaughlinGap.RealOccupation.rowTrace_tendsto line 41
  4. lemma OAI.LaughlinGap.RealOccupation.rowThreeTrace_tendsto line 60
  5. lemma OAI.LaughlinGap.RealOccupation.threeHighestAverage_eq line 65
  6. lemma OAI.LaughlinGap.RealOccupation.three_dimension_identity line 70
  7. theorem OAI.LaughlinGap.RealOccupation.three_comparison_of_strict_traces line 77