OAI/MathematicalPhysics/BFSS/FrequencyOperators.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantized-frequency commutators and self-adjointness.

  1. def OAI.BFSSQuantum.AlgebraData.thetaPair line 13
  2. lemma OAI.BFSSQuantum.AlgebraData.thetaPair_CAR line 15
  3. lemma OAI.BFSSQuantum.AlgebraData.thetaPair_product_commutator line 26
  4. theorem OAI.BFSSQuantum.AlgebraData.quantizeFrequency_commutator line 39
  5. lemma OAI.BFSSQuantum.AlgebraData.thetaPair_star line 103
  6. theorem OAI.BFSSQuantum.AlgebraData.quantizeFrequency_selfAdjoint line 106