OAI/Analysis/Laughlin/Charge/Sectors.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Charge.FockDegree line 10
  2. theorem OAI.Laughlin.Charge.fockDegree_sum line 13
  3. theorem OAI.Laughlin.Charge.fockDegree_smul line 20
  4. theorem OAI.Laughlin.Charge.fockDegree_annihilate line 25
  5. theorem OAI.Laughlin.Charge.fockDegree_create line 34
  6. theorem OAI.Laughlin.Charge.fockDegree_pair line 43
  7. theorem OAI.Laughlin.Charge.fockDegree_pairCreate line 54
  8. theorem OAI.Laughlin.Charge.fockDegree_hamiltonian line 65
  9. theorem OAI.Laughlin.Charge.hamiltonian_mem_sector line 73
  10. def OAI.Laughlin.Charge.sectorHamiltonian line 83
  11. theorem OAI.Laughlin.Charge.sectorHamiltonian_symmetric line 86
  12. theorem OAI.Laughlin.Charge.energy_eq_inner line 89
  13. theorem OAI.Laughlin.Charge.energy_eq_zero_iff line 95