OAI/Analysis/LaughlinFock/ThreeSpectrum.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Three Spectrum.

  1. theorem OAI.LaughlinFock.pairSwapCompression_apply line 15
  2. theorem OAI.LaughlinFock.pairSwapCompression_apply_fin line 37
  3. theorem OAI.LaughlinFock.threeWedgeMatrix_gram_mulVec_grid line 70
  4. def OAI.LaughlinFock.threeCoupledColumn line 117
  5. theorem OAI.LaughlinFock.threeWedgeMatrix_gram_eigenvector line 122
  6. theorem OAI.LaughlinFock.coupledVector_resolution line 135
  7. def OAI.LaughlinFock.threeCouplingMatrix line 150
  8. theorem OAI.LaughlinFock.threeCouplingMatrix_gram line 155
  9. theorem OAI.LaughlinFock.threeCouplingMatrix_complete line 185
  10. theorem OAI.LaughlinFock.threeWedgeMatrix_gram_diagonal line 200
  11. def OAI.LaughlinFock.threeSpinProjection line 229
  12. theorem OAI.LaughlinFock.threeSpinProjection_posSemidef line 234
  13. theorem OAI.LaughlinFock.threeSpinProjection_mul line 242
  14. theorem OAI.LaughlinFock.threeWedgeMatrix_gram_spectral line 271