OAI/Analysis/LaughlinFock/CrossOrbit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cross Orbit.

  1. def OAI.LaughlinFock.rotationCrossAverage line 25
  2. theorem OAI.LaughlinFock.rotationCrossOrbit_integrable line 28
  3. theorem OAI.LaughlinFock.rotationCrossAverage_invariant line 38
  4. theorem OAI.LaughlinFock.rotationCrossAverage_intertwines line 53
  5. theorem OAI.LaughlinFock.rotationCrossAverage_intertwines_generator line 63
  6. theorem OAI.LaughlinFock.rotationAverage_mixed_sandwich line 73
  7. theorem OAI.LaughlinFock.spinRotationCrossAverage_zero line 97
  8. theorem OAI.LaughlinFock.sectorAverage_spin_mixed_sandwich line 108
  9. theorem OAI.LaughlinFock.sectorAverage_spin_cross_sandwich line 122
  10. theorem OAI.LaughlinFock.fockAverage_spin_mixed_sandwich line 135