OAI/MathematicalPhysics/BFSS/CovariantFields.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Gauge covariance of Clifford symbols, fields and energy densities.

  1. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_coefficient line 14
  2. def OAI.BFSSQuantum.AlgebraData.colorClifford line 26
  3. def OAI.BFSSQuantum.AlgebraData.deformedColorCoefficient line 29
  4. lemma OAI.BFSSQuantum.AlgebraData.deformedColorCoefficient_apply line 35
  5. lemma OAI.BFSSQuantum.AlgebraData.deformedPotentialMultiplier_color line 52
  6. def OAI.BFSSQuantum.AlgebraData.principalColorCoefficient line 57
  7. lemma OAI.BFSSQuantum.AlgebraData.principalColorCoefficient_apply line 60
  8. lemma OAI.BFSSQuantum.AlgebraData.principalSymbol_color line 65
  9. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.colorClifford_covariant line 72
  10. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.spatialColor_boson line 86
  11. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedColorCoefficient_boson line 92
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedPotentialMultiplier_covariant line 99
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.principalColorCoefficient_boson line 106
  14. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.principalSymbol_covariant line 111
  15. def OAI.BFSSQuantum.AlgebraData.kineticSkewLinear line 125
  16. lemma OAI.BFSSQuantum.AlgebraData.kineticSkewLinear_basis line 133
  17. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.kineticSkewLinear_covariant line 138
  18. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedRealField_derivative_covariant line 146
  19. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedFermionField_covariant line 164
  20. def OAI.BFSSQuantum.AlgebraData.bosonicDensity line 200
  21. def OAI.BFSSQuantum.AlgebraData.fermionicDensity line 203
  22. lemma OAI.BFSSQuantum.AlgebraData.bosonicDensity_continuous line 206
  23. lemma OAI.BFSSQuantum.AlgebraData.fermionicDensity_continuous line 217
  24. lemma OAI.BFSSQuantum.AlgebraData.bosonicDensity_compactSupport line 221
  25. lemma OAI.BFSSQuantum.AlgebraData.fermionicDensity_compactSupport line 225
  26. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.fermion_real_inner line 236
  27. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_bosonicDensity line 241
  28. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_fermionicDensity line 247
  29. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_bosonicDensity_unitary line 252
  30. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_fermionicDensity_unitary line 259