OAI/Analysis/LaughlinFock/LadderCalculus.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Ladder Calculus.

  1. def OAI.LaughlinFock.spinStep line 13
  2. theorem OAI.LaughlinFock.spinStep_zero line 15
  3. theorem OAI.LaughlinFock.spinStep_cutoff line 17
  4. theorem OAI.LaughlinFock.spinStep_last line 23
  5. theorem OAI.LaughlinFock.spinStep_sq line 26
  6. theorem OAI.LaughlinFock.spinStep_sq_sub line 33
  7. theorem OAI.LaughlinFock.spinStep_pos line 39
  8. abbrev OAI.LaughlinFock.GridVector line 46
  9. def OAI.LaughlinFock.GridSupported line 48
  10. def OAI.LaughlinFock.GridLayer line 51
  11. def OAI.LaughlinFock.gridLower line 55
  12. def OAI.LaughlinFock.gridRaise line 59
  13. theorem OAI.LaughlinFock.gridLower_smul line 62
  14. theorem OAI.LaughlinFock.gridRaise_smul line 68
  15. theorem OAI.LaughlinFock.gridLower_zero line 74
  16. theorem OAI.LaughlinFock.gridRaise_zero line 78
  17. theorem OAI.LaughlinFock.gridLower_supported line 82
  18. theorem OAI.LaughlinFock.gridRaise_supported line 91
  19. theorem OAI.LaughlinFock.gridLower_layer line 98
  20. theorem OAI.LaughlinFock.grid_commutator_at line 114
  21. theorem OAI.LaughlinFock.grid_commutator_layer line 129
  22. def OAI.LaughlinFock.gridInner line 150
  23. theorem OAI.LaughlinFock.gridInner_smul_left line 153
  24. theorem OAI.LaughlinFock.gridInner_smul_right line 157
  25. theorem OAI.LaughlinFock.spinStep_sum_adjoint line 161
  26. theorem OAI.LaughlinFock.grid_adjoint line 172
  27. def OAI.LaughlinFock.coupledVector line 186
  28. theorem OAI.LaughlinFock.coupledVector_layer line 189
  29. theorem OAI.LaughlinFock.coupledVector_supported line 194
  30. theorem OAI.LaughlinFock.spinStep_succ line 204
  31. theorem OAI.LaughlinFock.coupledVector_highest line 214
  32. theorem OAI.LaughlinFock.coupledVector_succ_apply line 233
  33. theorem OAI.LaughlinFock.coupledVector_succ line 256
  34. theorem OAI.LaughlinFock.coupledVector_lower line 272
  35. theorem OAI.LaughlinFock.coupledVector_top_norm line 280
  36. theorem OAI.LaughlinFock.coupledVector_commutator line 315
  37. theorem OAI.LaughlinFock.coupledVector_raise line 327
  38. theorem OAI.LaughlinFock.coupledVector_norm line 363
  39. theorem OAI.LaughlinFock.gridInner_zero_right line 381
  40. theorem OAI.LaughlinFock.gridInner_zero_left line 384
  41. theorem OAI.LaughlinFock.gridInner_comm line 387
  42. theorem OAI.LaughlinFock.gridInner_of_layers line 391
  43. theorem OAI.LaughlinFock.coupledVector_orthogonal line 404
  44. theorem OAI.LaughlinFock.coupledVector_gram line 431