OAI/Analysis/Laughlin/Fock/ModeEmbedding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Fock.modeInclusion line 8
  2. def OAI.Laughlin.Fock.fockInclusion line 13
  3. def OAI.Laughlin.Fock.includedOccupations line 16
  4. theorem OAI.Laughlin.Fock.modeInclusion_mode line 19
  5. theorem OAI.Laughlin.Fock.fockInclusion_create line 41
  6. theorem OAI.Laughlin.Fock.contraction_map_between line 48
  7. theorem OAI.Laughlin.Fock.fockInclusion_annihilate line 61
  8. theorem OAI.Laughlin.Fock.fockInclusion_annihilate_high line 74
  9. theorem OAI.Laughlin.Fock.fockInclusion_occupation line 85
  10. theorem OAI.Laughlin.Fock.includedOccupations_injective line 121
  11. theorem OAI.Laughlin.Fock.fockInclusion_inner line 124
  12. theorem OAI.Laughlin.Fock.fockInclusion_normSq line 138