OAI/Analysis/LaughlinFock/RationalFour.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational Four.

  1. def OAI.LaughlinFock.rationalCopyDiagonal line 13
  2. def OAI.LaughlinFock.rationalCopyPolynomial line 16
  3. def OAI.LaughlinFock.rationalCopyWeight line 21
  4. theorem OAI.LaughlinFock.rationalCopyDiagonal_pos line 25
  5. theorem OAI.LaughlinFock.rationalCopyWeight_pos line 29
  6. theorem OAI.LaughlinFock.couplingWeight_copy line 33
  7. theorem OAI.LaughlinFock.planarCopyCoefficient_rational line 50
  8. def OAI.LaughlinFock.rationalFourFactor line 82
  9. theorem OAI.LaughlinFock.rationalFourFactor_pos line 87
  10. theorem OAI.LaughlinFock.row_copy_weight_product line 92
  11. def OAI.LaughlinFock.rationalFourTrace line 115
  12. theorem OAI.LaughlinFock.planarRowFourTrace_rational line 123