OAI/Analysis/LaughlinGap/RationalFourCertificate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Rational Four Certificate.

  1. def OAI.LaughlinGap.RealOccupation.copyNormalizationSq line 18
  2. lemma OAI.LaughlinGap.RealOccupation.copyNormalization_sq line 20
  3. def OAI.LaughlinGap.RealOccupation.rationalFourComparison line 24
  4. def OAI.LaughlinGap.RealOccupation.rationalFourCompression line 30
  5. def OAI.LaughlinGap.RealOccupation.copyDiagonal line 34
  6. lemma OAI.LaughlinGap.RealOccupation.createdGram_eq_diagonal line 37
  7. lemma OAI.LaughlinGap.RealOccupation.rationalFourComparison_real line 46
  8. lemma OAI.LaughlinGap.RealOccupation.rationalFourComparison_eq line 73
  9. lemma OAI.LaughlinGap.RealOccupation.fourCertificate_of_rational line 85
  10. lemma OAI.LaughlinGap.RealOccupation.rational_ldl_positive line 98