OAI/Analysis/LaughlinGap/RationalRows.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Rational Rows.

  1. structure OAI.LaughlinGap.RealOccupation.RationalRow line 15
  2. def OAI.LaughlinGap.RealOccupation.rowNormalization line 20
  3. def OAI.LaughlinGap.RealOccupation.RationalRow.toReal line 24
  4. def OAI.LaughlinGap.RealOccupation.threeRowScale line 29
  5. def OAI.LaughlinGap.RealOccupation.threeRowFactor line 33
  6. lemma OAI.LaughlinGap.RealOccupation.sqrt_natpow_sq line 37
  7. lemma OAI.LaughlinGap.RealOccupation.threeRowScale_sq line 40
  8. lemma OAI.LaughlinGap.RealOccupation.rowNormalization_three line 48
  9. lemma OAI.LaughlinGap.RealOccupation.threeWeight_row_t line 61
  10. lemma OAI.LaughlinGap.RealOccupation.sum_fibers_multiply line 69
  11. lemma OAI.LaughlinGap.RealOccupation.sum_fibers_trace line 76
  12. lemma OAI.LaughlinGap.RealOccupation.rowTrace_regroup line 90
  13. def OAI.LaughlinGap.RealOccupation.RationalRow.threeSum line 120
  14. def OAI.LaughlinGap.RealOccupation.RationalRow.threeTrace line 124
  15. lemma OAI.LaughlinGap.RealOccupation.RationalRow.threeSum_normalized line 128
  16. lemma OAI.LaughlinGap.RealOccupation.RationalRow.threeTrace_eq line 144