OAI/Analysis/LaughlinFock/ExchangeSpectrum.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exchange Spectrum.

  1. theorem OAI.LaughlinFock.sphericalPairCoefficient_coupled line 13
  2. theorem OAI.LaughlinFock.sphericalPairCoefficient_top line 18
  3. theorem OAI.LaughlinFock.pairCoupled_top line 29
  4. theorem OAI.LaughlinFock.pairTensorProject_top line 37
  5. theorem OAI.LaughlinFock.pairTensorEmbed_apply line 47
  6. theorem OAI.LaughlinFock.pairTensorEmbed_zero_zero line 57
  7. theorem OAI.LaughlinFock.pairSwapCompression_highest line 66
  8. theorem OAI.LaughlinFock.pairSwapCompression_highest_zero line 86
  9. theorem OAI.LaughlinFock.sphericalPairCoefficient_edge_one line 100
  10. theorem OAI.LaughlinFock.sphericalPairCoefficient_edge_zero line 112
  11. theorem OAI.LaughlinFock.sqrt_mul_sqrt_div line 130
  12. theorem OAI.LaughlinFock.fallingRatio_penultimate line 138
  13. theorem OAI.LaughlinFock.pairSwapCompression_scalar line 163
  14. theorem OAI.LaughlinFock.pairSwapCompression_eigenvector line 206