OAI/MathematicalPhysics/BFSS/Core.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

The full-space Hilbert model, exact smooth supercharges and closure of the joint graph.

  1. abbrev OAI.BFSSQuantum.colorDim line 12
  2. abbrev OAI.BFSSQuantum.ColorIndex line 13
  3. abbrev OAI.BFSSQuantum.SpaceIndex line 14
  4. abbrev OAI.BFSSQuantum.SpinIndex line 15
  5. abbrev OAI.BFSSQuantum.Boson line 16
  6. abbrev OAI.BFSSQuantum.Fermion line 17
  7. abbrev OAI.BFSSQuantum.ColorMatrix line 18
  8. abbrev OAI.BFSSQuantum.GammaMatrix line 19
  9. abbrev OAI.BFSSQuantum.GaugeGroup line 20
  10. abbrev OAI.BFSSQuantum.FullL2 line 21
  11. abbrev OAI.BFSSQuantum.SmoothCore line 22
  12. structure OAI.BFSSQuantum.AlgebraData line 24
  13. def OAI.BFSSQuantum.AlgebraData.bracket line 45
  14. def OAI.BFSSQuantum.AlgebraData.structureConstant line 48
  15. def OAI.BFSSQuantum.AlgebraData.gammaTwo line 51
  16. def OAI.BFSSQuantum.AlgebraData.polarization line 54
  17. def OAI.BFSSQuantum.AlgebraData.smoothMultiplier line 56
  18. def OAI.BFSSQuantum.AlgebraData.coordinateDerivative line 77
  19. def OAI.BFSSQuantum.AlgebraData.coordinate line 80
  20. lemma OAI.BFSSQuantum.AlgebraData.coordinate_contDiff line 82
  21. def OAI.BFSSQuantum.AlgebraData.position line 86
  22. def OAI.BFSSQuantum.AlgebraData.fermionAction line 90
  23. def OAI.BFSSQuantum.AlgebraData.charge line 93
  24. def OAI.BFSSQuantum.AlgebraData.coreToL2 line 102
  25. def OAI.BFSSQuantum.AlgebraData.chargeVector line 107
  26. def OAI.BFSSQuantum.AlgebraData.coreForm line 110
  27. lemma OAI.BFSSQuantum.AlgebraData.coreForm_nonneg line 113
  28. lemma OAI.BFSSQuantum.AlgebraData.coreToL2_ae line 116
  29. lemma OAI.BFSSQuantum.AlgebraData.coreToL2_inner line 120
  30. lemma OAI.BFSSQuantum.AlgebraData.coreToL2_dense line 127
  31. lemma OAI.BFSSQuantum.AlgebraData.coreInner_integrable line 135
  32. def OAI.BFSSQuantum.AlgebraData.innerRealLinear line 140
  33. def OAI.BFSSQuantum.AlgebraData.innerRealBilin line 148
  34. lemma OAI.BFSSQuantum.AlgebraData.coordinateDerivative_apply line 154
  35. lemma OAI.BFSSQuantum.AlgebraData.coordinateDerivative_skew line 162
  36. def OAI.BFSSQuantum.AlgebraData.CoreSymmetric line 175
  37. lemma OAI.BFSSQuantum.AlgebraData.coreSymmetric_add line 179
  38. lemma OAI.BFSSQuantum.AlgebraData.coreSymmetric_real_smul line 185
  39. lemma OAI.BFSSQuantum.AlgebraData.coreSymmetric_sum line 192
  40. lemma OAI.BFSSQuantum.AlgebraData.coreSymmetric_comp line 199
  41. lemma OAI.BFSSQuantum.AlgebraData.fermionAction_symmetric line 207
  42. lemma OAI.BFSSQuantum.AlgebraData.position_symmetric line 215
  43. lemma OAI.BFSSQuantum.AlgebraData.momentum_symmetric line 225
  44. lemma OAI.BFSSQuantum.AlgebraData.fermionAction_position_commute line 234
  45. lemma OAI.BFSSQuantum.AlgebraData.position_commute line 246
  46. lemma OAI.BFSSQuantum.AlgebraData.fermionAction_derivative_commute line 256
  47. lemma OAI.BFSSQuantum.AlgebraData.kineticTerm_symmetric line 274
  48. lemma OAI.BFSSQuantum.AlgebraData.potentialTerm_symmetric line 285
  49. theorem OAI.BFSSQuantum.AlgebraData.charge_symmetric line 294
  50. def OAI.BFSSQuantum.AlgebraData.fullCoreGraph line 318
  51. def OAI.BFSSQuantum.AlgebraData.fullClosedGraph line 321
  52. lemma OAI.BFSSQuantum.AlgebraData.fullClosedGraph_pairing line 324
  53. theorem OAI.BFSSQuantum.AlgebraData.fullClosedGraph_vertical line 337
  54. lemma OAI.BFSSQuantum.AlgebraData.fullClosedGraph_unique line 345