OAI/Analysis/LaughlinFock/FiniteComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite Comparison.

  1. def OAI.LaughlinFock.rowsEta line 14
  2. def OAI.LaughlinFock.rowsThreeTrace line 18
  3. def OAI.LaughlinFock.planarRowsThreeTrace line 22
  4. theorem OAI.LaughlinFock.rowsThreeTrace_tendsto line 25
  5. abbrev OAI.LaughlinFock.ComparedThreeBlock line 32
  6. theorem OAI.LaughlinFock.rowsThreeTrace_eventual_bound line 36
  7. def OAI.LaughlinFock.finiteThreeTarget line 60
  8. def OAI.LaughlinFock.fullThreeTarget line 66
  9. def OAI.LaughlinFock.threeTraceForm line 73
  10. theorem OAI.LaughlinFock.threeWedgeMatrix_null_sandwich line 79
  11. theorem OAI.LaughlinFock.threeTraceForm_le_finite_of_coefficients line 88
  12. theorem OAI.LaughlinFock.threeTraceForm_eventual_bound line 112