OAI/Analysis/LaughlinFock/ThreeTraces.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Three Traces.

  1. def OAI.LaughlinFock.sourceRowP line 13
  2. def OAI.LaughlinFock.sourceRowI line 16
  3. def OAI.LaughlinFock.sourceRowJ line 19
  4. def OAI.LaughlinFock.sourceRowT line 22
  5. def OAI.LaughlinFock.sourceRowThreeKernel line 26
  6. theorem OAI.LaughlinFock.sourceRowThreeKernel_lift line 31
  7. def OAI.LaughlinFock.sphericalRowAmplitude line 39
  8. theorem OAI.LaughlinFock.coupledVector_eq_sphericalThree line 44
  9. theorem OAI.LaughlinFock.sourceRowThreeKernel_diagonal line 51
  10. theorem OAI.LaughlinFock.sphericalRowAmplitude_zero line 87
  11. def OAI.LaughlinFock.rowThreeLevelTrace line 96
  12. theorem OAI.LaughlinFock.rowThreeLevelTrace_lower_zero line 102
  13. theorem OAI.LaughlinFock.rowThreeLevelTrace_upper_zero line 106
  14. theorem OAI.LaughlinFock.sourceRowThreeKernel_diagonal_level line 110
  15. theorem OAI.LaughlinFock.sum_shifted_of_support line 125
  16. theorem OAI.LaughlinFock.sourceRowThreeKernel_spinTrace line 138
  17. theorem OAI.LaughlinFock.threeSpinProjection_kernel_trace line 155
  18. theorem OAI.LaughlinFock.sourceRowThreeKernel_projectionTrace line 187
  19. theorem OAI.LaughlinFock.rowThreeTrace_above_support line 196