OAI/MathematicalPhysics/BFSS/MassIdentity.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Weighted mass-spin identities and rotation generators.

  1. def OAI.BFSSGamma.firstThree line 16
  2. def OAI.BFSSGamma.massWeight line 17
  3. def OAI.BFSSGamma.massT line 18
  4. def OAI.BFSSGamma.skew line 19
  5. def OAI.BFSSGamma.massC line 20
  6. def OAI.BFSSGamma.massR line 22
  7. def OAI.BFSSGamma.rotationSpin line 24
  8. def OAI.BFSSGamma.MassSpinIdentity line 27
  9. lemma OAI.BFSSGamma.firstThree_sort line 31
  10. lemma OAI.BFSSGamma.firstThree_card line 36
  11. lemma OAI.BFSSGamma.mem_firstThree line 38
  12. lemma OAI.BFSSGamma.massWeight_sum line 44
  13. lemma OAI.BFSSGamma.word_firstThree line 47
  14. lemma OAI.BFSSGamma.massT_transpose line 51
  15. lemma OAI.BFSSGamma.massT_sq line 56
  16. lemma OAI.BFSSGamma.gamma_massT_conj line 69
  17. lemma OAI.BFSSGamma.gamma_massT_comm line 76
  18. lemma OAI.BFSSGamma.skew_transpose line 85
  19. lemma OAI.BFSSGamma.massC_skew line 90
  20. lemma OAI.BFSSGamma.trace_skew_outer line 95
  21. lemma OAI.BFSSGamma.weighted_word_conj line 105
  22. lemma OAI.BFSSGamma.mass_trace_word line 123
  23. lemma OAI.BFSSGamma.word_pair line 160
  24. lemma OAI.BFSSGamma.word_trace_dual line 164
  25. lemma OAI.BFSSGamma.mass_stats line 172
  26. lemma OAI.BFSSGamma.mass_weight_stats line 177
  27. lemma OAI.BFSSGamma.mass_sign_stats line 184
  28. lemma OAI.BFSSGamma.massT_gamma_comm line 191
  29. lemma OAI.BFSSGamma.massT_list_comm line 199
  30. lemma OAI.BFSSGamma.massT_word_comm line 212
  31. lemma OAI.BFSSGamma.word_massT_transpose line 219
  32. lemma OAI.BFSSGamma.thirdWord_no_outside line 226
  33. lemma OAI.BFSSGamma.thirdWord_mass_pair line 237
  34. lemma OAI.BFSSGamma.gamma_pair_mass_transpose line 293
  35. lemma OAI.BFSSGamma.mass_pair_weight_cancel line 304
  36. lemma OAI.BFSSGamma.massR_diag line 320
  37. lemma OAI.BFSSGamma.massR_skew line 323
  38. lemma OAI.BFSSGamma.rotationSpin_skew line 332
  39. lemma OAI.BFSSGamma.trace_dual_pair line 345
  40. lemma OAI.BFSSGamma.trace_rotationSpin_other line 351
  41. lemma OAI.BFSSGamma.sorted_pair_unique line 382
  42. lemma OAI.BFSSGamma.trace_pair_pair line 396
  43. lemma OAI.BFSSGamma.trace_rotationSpin_pair line 431
  44. lemma OAI.BFSSGamma.mass_pair_trace line 452
  45. def OAI.BFSSGamma.massRHS line 465
  46. lemma OAI.BFSSGamma.massRHS_skew line 468
  47. lemma OAI.BFSSGamma.trace_symm_skew line 474
  48. lemma OAI.BFSSGamma.mass_identity_trace_word line 479
  49. theorem OAI.BFSSGamma.mass_spin_identity line 516