OAI/Analysis/LaughlinFock/NumericTrace.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Numeric Trace.

  1. structure OAI.LaughlinFock.NumericRowEntry line 12
  2. def OAI.LaughlinFock.rowToNumeric line 19
  3. def OAI.LaughlinFock.numericRowData_0 line 22
  4. theorem OAI.LaughlinFock.numericRowDataChecked_0 line 69
  5. def OAI.LaughlinFock.numericRowData_1 line 73
  6. theorem OAI.LaughlinFock.numericRowDataChecked_1 line 126
  7. def OAI.LaughlinFock.numericRowData_2 line 130
  8. theorem OAI.LaughlinFock.numericRowDataChecked_2 line 187
  9. def OAI.LaughlinFock.numericRowData_3 line 191
  10. theorem OAI.LaughlinFock.numericRowDataChecked_3 line 250
  11. def OAI.LaughlinFock.numericRowData_4 line 254
  12. theorem OAI.LaughlinFock.numericRowDataChecked_4 line 313
  13. def OAI.LaughlinFock.numericRowData_5 line 317
  14. theorem OAI.LaughlinFock.numericRowDataChecked_5 line 374
  15. def OAI.LaughlinFock.numericRowData_6 line 378
  16. theorem OAI.LaughlinFock.numericRowDataChecked_6 line 431
  17. def OAI.LaughlinFock.numericRowData_7 line 435
  18. theorem OAI.LaughlinFock.numericRowDataChecked_7 line 482
  19. def OAI.LaughlinFock.numericRowData line 486
  20. theorem OAI.LaughlinFock.sum_table line 489
  21. theorem OAI.LaughlinFock.numericRow_sum line 496
  22. def OAI.LaughlinFock.numericRowFactor line 508
  23. def OAI.LaughlinFock.numericRowTerm line 513
  24. def OAI.LaughlinFock.numericFourTrace line 520
  25. theorem OAI.LaughlinFock.memoScaledFourTrace_numeric line 524
  26. def OAI.LaughlinFock.numericRowsFourTrace line 534
  27. theorem OAI.LaughlinFock.integerRowsFourTrace_numeric line 537