OAI/Analysis/Laughlin/Operators/PositiveFockLift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.occupationInner_star line 11
  2. theorem OAI.Laughlin.Fock.create_annihilate_adjoint_right line 15
  3. theorem OAI.Laughlin.Fock.pairCreate_pair_adjoint_right line 20
  4. def OAI.Laughlin.Fock.operatorLift line 26
  5. theorem OAI.Laughlin.Fock.operatorLift_quadratic line 30
  6. theorem OAI.Laughlin.Fock.operatorLift_positive line 51
  7. def OAI.Laughlin.Fock.sourceFourCreateEnd line 60
  8. theorem OAI.Laughlin.Fock.sourceFour_adjoint_right line 63
  9. theorem OAI.Laughlin.Fock.sourceFourLift_positive line 69