OAI/Analysis/LaughlinFock/SwapCompression.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Swap Compression.

  1. abbrev OAI.LaughlinFock.CubeVector line 11
  2. def OAI.LaughlinFock.CubeLayer line 13
  3. def OAI.LaughlinFock.cubeLower line 16
  4. def OAI.LaughlinFock.cubeRaise line 20
  5. def OAI.LaughlinFock.pairTensorEmbed line 26
  6. def OAI.LaughlinFock.pairTensorProject line 40
  7. def OAI.LaughlinFock.swap23 line 55
  8. def OAI.LaughlinFock.pairSwapCompression line 61
  9. theorem OAI.LaughlinFock.pairCoupled_lower line 64
  10. theorem OAI.LaughlinFock.pairCoupled_raise line 69
  11. theorem OAI.LaughlinFock.gridInner_add_right line 74
  12. theorem OAI.LaughlinFock.grid_raise_adjoint line 78
  13. theorem OAI.LaughlinFock.pairTensorProject_lower line 82
  14. theorem OAI.LaughlinFock.pairTensorProject_raise line 91
  15. theorem OAI.LaughlinFock.pairTensorEmbed_lower line 100
  16. theorem OAI.LaughlinFock.pairTensorEmbed_raise line 126
  17. theorem OAI.LaughlinFock.swap23_lower line 155
  18. theorem OAI.LaughlinFock.swap23_raise line 161
  19. theorem OAI.LaughlinFock.pairSwapCompression_lower line 169
  20. theorem OAI.LaughlinFock.pairSwapCompression_raise line 175
  21. theorem OAI.LaughlinFock.pairTensorEmbed_layer line 181
  22. theorem OAI.LaughlinFock.swap23_layer line 191
  23. theorem OAI.LaughlinFock.pairTensorProject_layer line 196
  24. theorem OAI.LaughlinFock.pairSwapCompression_layer line 208
  25. theorem OAI.LaughlinFock.pairSwapCompression_coupled line 214