OAI/MathematicalPhysics/BFSS/FermionQuantization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Quadratic Clifford quantization of the deformed fermion multiplier.

  1. def OAI.BFSSQuantum.AlgebraData.bracketComplex line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.bracketComplex_restrict line 19
  3. lemma OAI.BFSSQuantum.AlgebraData.coordinate_single_contraction line 23
  4. lemma OAI.BFSSQuantum.AlgebraData.kinetic_bracket_right line 35
  5. lemma OAI.BFSSQuantum.AlgebraData.kinetic_bracket_left line 58
  6. lemma OAI.BFSSQuantum.AlgebraData.kinetic_pairGamma_first line 82
  7. lemma OAI.BFSSQuantum.AlgebraData.kinetic_pairGamma_second line 93
  8. def OAI.BFSSQuantum.AlgebraData.cubicFermionComponent line 111
  9. lemma OAI.BFSSQuantum.AlgebraData.kinetic_bracket_average_right line 118
  10. lemma OAI.BFSSQuantum.AlgebraData.kinetic_bracket_average_left line 137
  11. lemma OAI.BFSSQuantum.AlgebraData.kinetic_bracket_average line 164
  12. lemma OAI.BFSSQuantum.AlgebraData.deformedFermionField_linear_parameters line 187
  13. lemma OAI.BFSSQuantum.AlgebraData.deformedFermionField_bracket line 195
  14. def OAI.BFSSQuantum.AlgebraData.fermionCoefficient line 236
  15. def OAI.BFSSQuantum.AlgebraData.quantizeFrequency line 241
  16. lemma OAI.BFSSQuantum.AlgebraData.sum_rotate_six line 253
  17. lemma OAI.BFSSQuantum.AlgebraData.frequency_mass_contraction line 263
  18. lemma OAI.BFSSQuantum.AlgebraData.frequency_bracket_contraction line 286
  19. theorem OAI.BFSSQuantum.AlgebraData.deformedFermionField_quantized line 331