OAI/Analysis/CoulombIonization/Fermionic/SlaterOccupation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombAtom.Occupied line 17
  2. def OAI.CoulombAtom.occupationIndex line 19
  3. def OAI.CoulombAtom.occupationOrbitals line 22
  4. lemma OAI.CoulombAtom.occupationIndex_sum line 25
  5. lemma OAI.CoulombAtom.occupationIndex_pair_sum line 36
  6. lemma OAI.CoulombAtom.occupationOrbitals_sum line 54
  7. lemma OAI.CoulombAtom.occupationOrbitals_smooth line 59
  8. lemma OAI.CoulombAtom.occupationOrbitals_compact line 64
  9. lemma OAI.CoulombAtom.occupationOrbitals_orthonormal line 69
  10. theorem OAI.CoulombAtom.occupationSlater_admissible line 79
  11. def OAI.CoulombAtom.orbitalCoreInteraction line 90
  12. lemma OAI.CoulombAtom.core_orbital_integrable line 94
  13. lemma OAI.CoulombAtom.blockTensorCross_slater line 112
  14. lemma OAI.CoulombAtom.occupationSlater_cross line 136