OAI/MathematicalPhysics/BFSS/FermionFrequency.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The exact skew normal fermion frequency and absence of zero frequencies.

  1. def OAI.BFSSQuantum.AlgebraData.spinHalf line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.spinHalf_skew line 17
  3. lemma OAI.BFSSQuantum.AlgebraData.spinHalf_sq line 27
  4. lemma OAI.BFSSQuantum.AlgebraData.spinHalf_product line 44
  5. lemma OAI.BFSSQuantum.AlgebraData.spinHalf_cyclic line 55
  6. lemma OAI.BFSSQuantum.AlgebraData.spinHalf_reverse line 75
  7. def OAI.BFSSQuantum.AlgebraData.colorJ line 83
  8. lemma OAI.BFSSQuantum.AlgebraData.colorJ_skew line 86
  9. lemma OAI.BFSSQuantum.AlgebraData.colorJ_commutators line 91
  10. abbrev OAI.BFSSQuantum.AlgebraData.FrequencyIndex line 118
  11. abbrev OAI.BFSSQuantum.AlgebraData.FrequencyMatrix line 119
  12. def OAI.BFSSQuantum.AlgebraData.colorJTensor line 121
  13. def OAI.BFSSQuantum.AlgebraData.spinHalfTensor line 124
  14. def OAI.BFSSQuantum.AlgebraData.spinHalfCoupling line 126
  15. lemma OAI.BFSSQuantum.AlgebraData.colorJTensor_skew line 130
  16. lemma OAI.BFSSQuantum.AlgebraData.spinHalfTensor_skew line 137
  17. lemma OAI.BFSSQuantum.AlgebraData.tensor_commute line 141
  18. lemma OAI.BFSSQuantum.AlgebraData.spinHalfCoupling_symmetric line 145
  19. lemma OAI.BFSSQuantum.AlgebraData.spinHalfCoupling_polynomial line 151
  20. def OAI.BFSSQuantum.AlgebraData.normalFermionFrequency line 181
  21. lemma OAI.BFSSQuantum.AlgebraData.massT_spinHalf line 186
  22. lemma OAI.BFSSQuantum.AlgebraData.normalFermionFrequency_factor line 192
  23. theorem OAI.BFSSQuantum.AlgebraData.normalFermionFrequency_trivial_kernel line 219
  24. lemma OAI.BFSSPairSum.endpoints line 242