OAI/MathematicalPhysics/BFSS/CliffordSymbols.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Clifford linear symbols, spin contractions and charge multiplier identities.

  1. abbrev OAI.BFSSQuantum.AlgebraData.FermionIndex line 15
  2. def OAI.BFSSQuantum.AlgebraData.cliffordLinear line 17
  3. lemma OAI.BFSSQuantum.AlgebraData.cliffordLinear_mixed line 20
  4. lemma OAI.BFSSQuantum.AlgebraData.cliffordLinear_sq line 51
  5. lemma OAI.BFSSQuantum.AlgebraData.cliffordLinear_selfAdjoint line 61
  6. lemma OAI.BFSSQuantum.AlgebraData.cliffordLinear_norm_sq line 72
  7. def OAI.BFSSQuantum.AlgebraData.gammaLinear line 88
  8. lemma OAI.BFSSQuantum.AlgebraData.gammaLinear_mixed line 90
  9. lemma OAI.BFSSQuantum.AlgebraData.gammaLinear_sq line 124
  10. lemma OAI.BFSSQuantum.AlgebraData.gammaLinear_symmetric line 133
  11. lemma OAI.BFSSQuantum.AlgebraData.gammaLinear_mulVec_sq line 141
  12. def OAI.BFSSQuantum.AlgebraData.principalCoefficients line 150
  13. def OAI.BFSSQuantum.AlgebraData.principalSymbol line 153
  14. lemma OAI.BFSSQuantum.AlgebraData.principalCoefficients_sq line 156
  15. lemma OAI.BFSSQuantum.AlgebraData.principalSymbol_sq line 166
  16. lemma OAI.BFSSQuantum.AlgebraData.principalSymbol_norm_sq line 175
  17. lemma OAI.BFSSQuantum.AlgebraData.principalSymbol_unit_norm_sq line 181
  18. lemma OAI.BFSSQuantum.AlgebraData.coordinateDerivative_multiplier line 186
  19. lemma OAI.BFSSQuantum.AlgebraData.fermionAction_apply line 198
  20. lemma OAI.BFSSQuantum.AlgebraData.smoothMultiplier_apply line 201
  21. lemma OAI.BFSSQuantum.AlgebraData.position_apply line 205
  22. lemma OAI.BFSSQuantum.AlgebraData.charge_apply line 208
  23. lemma OAI.BFSSQuantum.AlgebraData.charge_multiplier line 221
  24. def OAI.BFSSQuantum.AlgebraData.realCutoff line 238
  25. def OAI.BFSSQuantum.AlgebraData.cutoffGradient line 243
  26. lemma OAI.BFSSQuantum.AlgebraData.realCutoff_derivative line 246
  27. lemma OAI.BFSSQuantum.AlgebraData.principalCoefficients_basis line 253
  28. lemma OAI.BFSSQuantum.AlgebraData.principalSymbol_basis_apply line 264
  29. lemma OAI.BFSSQuantum.AlgebraData.charge_realCutoff line 280
  30. def OAI.BFSSQuantum.AlgebraData.principalSymbolLinear line 300
  31. lemma OAI.BFSSQuantum.AlgebraData.basisSpinor_unit line 322