OAI/Analysis/CoulombIonization/Fermionic/SlaterPairAlgebra.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.permutations_eq_or_swap_of_agree_except_two line 17
  2. abbrev OAI.CoulombAtom.SlaterPairRest line 44
  3. def OAI.CoulombAtom.slaterRestTensor line 46
  4. def OAI.CoulombAtom.slaterPairAmplitude line 50
  5. def OAI.CoulombAtom.slaterPairSliceRaw line 54
  6. lemma OAI.CoulombAtom.memLp_slaterRestTensor line 61
  7. lemma OAI.CoulombAtom.slaterRestTensor_inner line 75
  8. lemma OAI.CoulombAtom.perm_mul_swap_ne_self line 100
  9. lemma OAI.CoulombAtom.complex_sign_mul_swap line 107
  10. lemma OAI.CoulombAtom.slaterPairSliceRaw_norm_sq_integral line 111
  11. def OAI.CoulombAtom.slaterPairIndex line 150
  12. def OAI.CoulombAtom.slaterRestIndex line 161
  13. def OAI.CoulombAtom.slaterPairSplit line 170
  14. lemma OAI.CoulombAtom.slaterPairSplit_preserving line 179
  15. lemma OAI.CoulombAtom.slaterPairSplit_apply line 190
  16. lemma OAI.CoulombAtom.slaterPairSplit_symm_apply_left line 194
  17. lemma OAI.CoulombAtom.slaterPairSplit_symm_apply_right line 201
  18. lemma OAI.CoulombAtom.slaterPairSplit_symm_apply_rest line 208