OAI/Analysis/Laughlin/Charge/Model.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Laughlin.Charge.Hilbert line 11
  2. def OAI.Laughlin.Charge.particleSector line 13
  3. def OAI.Laughlin.Charge.energy line 19
  4. def OAI.Laughlin.Charge.unitSector line 22
  5. def OAI.Laughlin.Charge.groundEnergy line 25
  6. def OAI.Laughlin.Charge.groundKernel line 27
  7. def OAI.Laughlin.Charge.neutralGap line 30
  8. def OAI.Laughlin.Charge.chargeGap line 33
  9. def OAI.Laughlin.Charge.annihilator line 36
  10. def OAI.Laughlin.Charge.groundOverlap line 40
  11. theorem OAI.Laughlin.Charge.energy_nonneg line 43
  12. theorem OAI.Laughlin.Charge.groundEnergy_nonneg line 47
  13. theorem OAI.Laughlin.Charge.neutralGap_nonneg line 52
  14. theorem OAI.Laughlin.Charge.unitSector_nonempty line 57
  15. theorem OAI.Laughlin.Charge.groundEnergy_le line 73
  16. theorem OAI.Laughlin.Charge.groundEnergy_eq_zero_of_zero_mode line 81