OAI/MathematicalPhysics/BFSS/ColorMatrices.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Orthonormal color coordinates and the literal matrix potential.

  1. def OAI.BFSSQuantum.AlgebraData.colorCombination line 16
  2. def OAI.BFSSQuantum.AlgebraData.matrixCoordinate line 19
  3. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_hermitian line 22
  4. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_traceless line 30
  5. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_pairing line 34
  6. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_normSq line 43
  7. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_coeff line 50
  8. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_reconstruct line 56
  9. lemma OAI.BFSSQuantum.AlgebraData.bracket_hermitian line 64
  10. lemma OAI.BFSSQuantum.AlgebraData.bracket_traceless line 73
  11. lemma OAI.BFSSQuantum.AlgebraData.bracket_sum_left line 77
  12. lemma OAI.BFSSQuantum.AlgebraData.bracket_sum_right line 81
  13. lemma OAI.BFSSQuantum.AlgebraData.bracket_smul line 85
  14. lemma OAI.BFSSQuantum.AlgebraData.bracket_colorCombination line 92
  15. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_sub line 127
  16. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_smul line 131
  17. lemma OAI.BFSSQuantum.AlgebraData.colorCombination_neg line 135
  18. def OAI.BFSSQuantum.AlgebraData.matrixConfiguration line 139
  19. lemma OAI.BFSSQuantum.AlgebraData.matrixConfiguration_norm line 143
  20. def OAI.BFSSQuantum.AlgebraData.coordinateBracketAll line 148
  21. lemma OAI.BFSSQuantum.AlgebraData.coordinate_bracket_matrix line 151
  22. lemma OAI.BFSSQuantum.AlgebraData.coordinate_bracket_norm line 156
  23. lemma OAI.BFSSQuantum.AlgebraData.coordinate_shifted_norm line 161
  24. lemma OAI.BFSSQuantum.AlgebraData.coordinateBracketAll_skew line 169