OAI/Analysis/LaughlinFock/Model.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Model.

  1. abbrev OAI.LaughlinFock.Orbital line 13

    Also declared: ComparatorChallenges/LaughlinFock.lean:28 (same declaration text).

  2. abbrev OAI.LaughlinFock.Occupation line 14

    Also declared: ComparatorChallenges/LaughlinFock.lean:29 (same declaration text).

  3. abbrev OAI.LaughlinFock.FockSpace line 15
  4. abbrev OAI.LaughlinFock.FockMatrix line 16

    Also declared: ComparatorChallenges/LaughlinFock.lean:30 (same declaration text).

  5. def OAI.LaughlinFock.tensorPairCoefficient line 19

    Also declared: ComparatorChallenges/LaughlinFock.lean:32 (same declaration text).

  6. def OAI.LaughlinFock.pairCoefficient line 23

    Also declared: ComparatorChallenges/LaughlinFock.lean:35 (same declaration text).

  7. def OAI.LaughlinFock.annihilator line 28

    Also declared: ComparatorChallenges/LaughlinFock.lean:38 (same declaration text).

  8. def OAI.LaughlinFock.pairAnnihilator line 35

    Also declared: ComparatorChallenges/LaughlinFock.lean:43 (same declaration text).

  9. def OAI.LaughlinFock.hamiltonian line 43

    Also declared: ComparatorChallenges/LaughlinFock.lean:49 (same declaration text).

  10. abbrev OAI.LaughlinFock.SectorOccupation line 48
  11. def OAI.LaughlinFock.sectorHamiltonian line 51
  12. def OAI.LaughlinFock.gammaStar line 56

    Also declared: ComparatorChallenges/LaughlinFock.lean:53 (same declaration text).

  13. def OAI.LaughlinFock.FockInequality line 59

    Also declared: ComparatorChallenges/LaughlinFock.lean:55 (same declaration text).

  14. theorem OAI.LaughlinFock.pairCoefficient_eq line 65
  15. theorem OAI.LaughlinFock.hamiltonian_posSemidef line 79
  16. theorem OAI.LaughlinFock.hamiltonian_isHermitian line 83
  17. theorem OAI.LaughlinFock.sectorHamiltonian_posSemidef line 87
  18. theorem OAI.LaughlinFock.gammaStar_gt_one_twenty_fifth line 92
  19. theorem OAI.LaughlinFock.final_margin_arithmetic line 97
  20. theorem OAI.LaughlinFock.annihilator_card line 104
  21. theorem OAI.LaughlinFock.annihilator_entry_eq_zero line 111
  22. theorem OAI.LaughlinFock.pairAnnihilator_entry_eq_zero line 117
  23. theorem OAI.LaughlinFock.hamiltonian_entry_eq_zero line 138
  24. theorem OAI.LaughlinFock.sectorHamiltonian_eq_zero_of_le_one line 153
  25. theorem OAI.LaughlinFock.sectorHamiltonian_zero_particles line 166
  26. theorem OAI.LaughlinFock.sectorHamiltonian_one_particle line 169
  27. theorem OAI.LaughlinFock.sectorHamiltonian_square line 174
  28. theorem OAI.LaughlinFock.sector_inequality_of_fock line 197
  29. theorem OAI.LaughlinFock.gram_quadratic_form line 207
  30. theorem OAI.LaughlinFock.hamiltonian_quadratic_form line 214
  31. theorem OAI.LaughlinFock.occupation_card_le line 226
  32. theorem OAI.LaughlinFock.sector_quadratic_form_decomposition line 231
  33. theorem OAI.LaughlinFock.posSemidef_of_sectors line 268
  34. theorem OAI.LaughlinFock.gapMatrix_entry_eq_zero line 282
  35. theorem OAI.LaughlinFock.fock_inequality_iff_sectors line 297