OAI/Analysis/Laughlin/Planar/DegreeRestriction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.sum_fin_castLE_of_high_zero line 10
  2. theorem OAI.Laughlin.Fock.pairEnd_fockInclusion line 27
  3. theorem OAI.Laughlin.Fock.pairCreateEnd_fockInclusion line 47
  4. def OAI.Laughlin.Fock.DegreeAtMost line 68
  5. theorem OAI.Laughlin.Fock.two_mem_weight_le line 71
  6. theorem OAI.Laughlin.Fock.pair_annihilate_high_degree line 84
  7. theorem OAI.Laughlin.Fock.pairEnd_high_degree line 106
  8. def OAI.Laughlin.Fock.restrictedSpherePairEnd line 118
  9. def OAI.Laughlin.Fock.restrictedSpherePairCreateEnd line 121
  10. def OAI.Laughlin.Fock.restrictedSphereHamiltonian line 124
  11. def OAI.Laughlin.Fock.restrictedSphereEnergy line 127
  12. theorem OAI.Laughlin.Fock.sourcePairEnd_fockInclusion line 130
  13. theorem OAI.Laughlin.Fock.restrictedSpherePairEnd_high_degree line 143
  14. theorem OAI.Laughlin.Fock.sourcePairCreateEnd_fockInclusion line 149
  15. theorem OAI.Laughlin.Fock.sum_range_eq_short line 166
  16. theorem OAI.Laughlin.Fock.sourceFockHamiltonian_fockInclusion line 174
  17. theorem OAI.Laughlin.Fock.sourceFockEnergy_fockInclusion line 197