OAI/Analysis/Laughlin/Fock/Hamiltonian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Fock.pairCreateEnd line 8
  2. theorem OAI.Laughlin.Fock.pairCreate_pair_adjoint line 11
  3. def OAI.Laughlin.Fock.sourcePairCreateEnd line 18
  4. def OAI.Laughlin.Fock.sourceFockHamiltonian line 21
  5. def OAI.Laughlin.Fock.sourceFockEnergy line 24
  6. theorem OAI.Laughlin.Fock.sourceFockHamiltonian_quadratic line 27
  7. theorem OAI.Laughlin.Fock.sourceFockHamiltonian_positive line 33
  8. theorem OAI.Laughlin.Fock.sourceFockEnergy_eq_zero line 40