OAI/MathematicalPhysics/BFSS/FermionModes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

CAR eigenmodes, actual ground vectors and lowering operators.

  1. def OAI.BFSSQuantum.AlgebraData.thetaMode line 15
  2. lemma OAI.BFSSQuantum.AlgebraData.thetaMode_smul line 18
  3. theorem OAI.BFSSQuantum.AlgebraData.thetaMode_CAR line 22
  4. lemma OAI.BFSSQuantum.AlgebraData.thetaMode_star line 57
  5. theorem OAI.BFSSQuantum.AlgebraData.thetaMode_commutator line 65
  6. theorem OAI.BFSSQuantum.AlgebraData.quantizeFrequency_ground_exists line 96
  7. theorem OAI.BFSSQuantum.AlgebraData.quantizeFrequency_ground_killed line 119
  8. theorem OAI.BFSSQuantum.AlgebraData.normal_fermion_ground_lowering line 143