OAI/Analysis/LaughlinFock/BesselComparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bessel Comparison.

  1. abbrev OAI.LaughlinFock.CopyLabel line 12
  2. abbrev OAI.LaughlinFock.FourUncoupled line 15
  3. abbrev OAI.LaughlinFock.FourHighestShell line 18
  4. theorem OAI.LaughlinFock.sum_subtype_support line 22
  5. def OAI.LaughlinFock.highestCopyMatrix line 35
  6. theorem OAI.LaughlinFock.highestCopyMatrix_gram line 41
  7. def OAI.LaughlinFock.shellFourAnnihilator line 66
  8. def OAI.LaughlinFock.highestFourAnnihilator line 71
  9. theorem OAI.LaughlinFock.highestFourAnnihilator_bessel line 76
  10. theorem OAI.LaughlinFock.highestFourAnnihilator_pair_bound line 87
  11. def OAI.LaughlinFock.fourHighestShellEquiv line 98
  12. theorem OAI.LaughlinFock.fourHighestShell_card_sum line 146
  13. theorem OAI.LaughlinFock.shell_count_formula line 153
  14. theorem OAI.LaughlinFock.fourHighestShell_card line 167
  15. theorem OAI.LaughlinFock.fourHighestShell_count line 173