OAI/MathematicalPhysics/BFSS/PotentialBasis.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal potential matrices and the averaged deformed bosonic potential.

  1. abbrev OAI.BFSSGamma.SpatialPair line 18
  2. abbrev OAI.BFSSGamma.TailIndex line 19
  3. def OAI.BFSSGamma.pairGamma line 20
  4. def OAI.BFSSGamma.shiftedPair line 22
  5. def OAI.BFSSGamma.bracketMassMatrix line 27
  6. lemma OAI.BFSSGamma.pairGamma_skew line 31
  7. lemma OAI.BFSSGamma.pairGamma_trace line 35
  8. lemma OAI.BFSSGamma.gamma_product_trace line 49
  9. lemma OAI.BFSSGamma.massT_mul_transpose line 54
  10. lemma OAI.BFSSGamma.gammaT_trace line 57
  11. lemma OAI.BFSSGamma.tailGamma_symmetric line 67
  12. lemma OAI.BFSSGamma.pair_tail_trace line 74
  13. lemma OAI.BFSSGamma.dual_trace_comm line 81
  14. lemma OAI.BFSSGamma.tail_pair_trace line 87
  15. def OAI.BFSSGamma.potentialBasis line 91
  16. lemma OAI.BFSSGamma.potentialBasis_trace line 96
  17. lemma OAI.BFSSGamma.trace_orthogonal_sum line 110
  18. lemma OAI.BFSSGamma.potential_orthogonal_sum line 124
  19. lemma OAI.BFSSGamma.gamma0_massT line 133
  20. lemma OAI.BFSSGamma.gamma1_massT line 138
  21. lemma OAI.BFSSGamma.gamma2_massT line 145
  22. lemma OAI.BFSSGamma.mass_sum_decomposition line 152
  23. def OAI.BFSSGamma.pair01 line 176
  24. def OAI.BFSSGamma.pair02 line 178
  25. def OAI.BFSSGamma.pair12 line 180
  26. lemma OAI.BFSSGamma.shiftedPair_sum line 183
  27. lemma OAI.BFSSGamma.bracketMass_decomposition line 202
  28. lemma OAI.BFSSGamma.bracketMass_trace_square line 211
  29. abbrev OAI.BFSSQuantum.AlgebraData.SpatialPair line 226
  30. abbrev OAI.BFSSQuantum.AlgebraData.TailIndex line 227
  31. def OAI.BFSSQuantum.AlgebraData.coordinateBracket line 229
  32. def OAI.BFSSQuantum.AlgebraData.deformedPotentialMatrix line 232
  33. def OAI.BFSSQuantum.AlgebraData.deformedPotentialCoefficients line 236
  34. def OAI.BFSSQuantum.AlgebraData.deformedPotentialMultiplier line 240
  35. def OAI.BFSSQuantum.AlgebraData.deformedBosonicPotential line 244
  36. lemma OAI.BFSSQuantum.AlgebraData.deformedPotentialMatrix_trace line 250
  37. lemma OAI.BFSSQuantum.AlgebraData.deformedPotentialCoefficients_total line 258
  38. theorem OAI.BFSSQuantum.AlgebraData.deformed_potential_average line 279