OAI/Analysis/LaughlinGap/ExactRows.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Exact Rows.

  1. def OAI.LaughlinGap.RealOccupation.rowLambdaInteger line 16
  2. def OAI.LaughlinGap.RealOccupation.rowAlphaInteger line 18
  3. def OAI.LaughlinGap.RealOccupation.exactRows line 29
  4. def OAI.LaughlinGap.RealOccupation.etaRational line 34
  5. lemma OAI.LaughlinGap.RealOccupation.etaRational_value line 36
  6. lemma OAI.LaughlinGap.RealOccupation.small_margin line 38
  7. lemma OAI.LaughlinGap.RealOccupation.test_sum line 42
  8. lemma OAI.LaughlinGap.RealOccupation.test_trace line 43
  9. def OAI.LaughlinGap.RealOccupation.traceRational line 52
  10. lemma OAI.LaughlinGap.RealOccupation.traceRational_eq line 57
  11. lemma OAI.LaughlinGap.RealOccupation.trace_bound_2 line 62
  12. lemma OAI.LaughlinGap.RealOccupation.trace_bound_4 line 63
  13. lemma OAI.LaughlinGap.RealOccupation.trace_bound_5 line 64
  14. lemma OAI.LaughlinGap.RealOccupation.trace_bound_6 line 65
  15. lemma OAI.LaughlinGap.RealOccupation.trace_bound_7 line 66
  16. lemma OAI.LaughlinGap.RealOccupation.trace_bound_8 line 67
  17. lemma OAI.LaughlinGap.RealOccupation.trace_bound_9 line 68
  18. lemma OAI.LaughlinGap.RealOccupation.trace_bound_10 line 69
  19. lemma OAI.LaughlinGap.RealOccupation.trace_bound_11 line 70
  20. lemma OAI.LaughlinGap.RealOccupation.trace_bound_12 line 71
  21. lemma OAI.LaughlinGap.RealOccupation.trace_bound_13 line 72
  22. lemma OAI.LaughlinGap.RealOccupation.trace_bound_14 line 73
  23. lemma OAI.LaughlinGap.RealOccupation.trace_bound_15 line 74
  24. lemma OAI.LaughlinGap.RealOccupation.exact_three line 76
  25. lemma OAI.LaughlinGap.RealOccupation.exact_margin line 102