OAI/Analysis/LaughlinGap/RationalCoupling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Rational Coupling.

  1. def OAI.LaughlinGap.Spin.rootFactorial line 15
  2. lemma OAI.LaughlinGap.Spin.rootFactorial_pos line 16
  3. lemma OAI.LaughlinGap.Spin.rootFactorial_ne_zero line 18
  4. lemma OAI.LaughlinGap.Spin.rootFactorial_sq line 19
  5. lemma OAI.LaughlinGap.Spin.rootFactorial_zero line 21
  6. lemma OAI.LaughlinGap.Spin.monomialWeight_roots line 23
  7. def OAI.LaughlinGap.Spin.integerCoupling line 26
  8. def OAI.LaughlinGap.Spin.uCoefficient line 28
  9. lemma OAI.LaughlinGap.Spin.integerCoupling_coeff line 32
  10. lemma OAI.LaughlinGap.Spin.uCoefficient_eq_coeff line 46
  11. lemma OAI.LaughlinGap.Spin.couplingPolynomial_equal line 50
  12. lemma OAI.LaughlinGap.Spin.balancedCouplingCoefficient_rational line 65
  13. lemma OAI.LaughlinGap.Spin.couplingPolynomial_scaled line 76
  14. lemma OAI.LaughlinGap.Spin.threeWeightCoefficientStar_rational line 97