OAI/Analysis/CoulombIonization/Fermionic/Slater.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.CoulombAtom.slaterTensorline 18 - def
OAI.CoulombAtom.slaterRawline 21 - lemma
OAI.CoulombAtom.slaterRaw_eq_detline 25 - lemma
OAI.CoulombAtom.memLp_slaterTensorline 30 - lemma
OAI.CoulombAtom.memLp_slaterRawline 43 - lemma
OAI.CoulombAtom.slaterTensor_innerline 47 - lemma
OAI.CoulombAtom.permutations_eq_of_agree_exceptline 55 - lemma
OAI.CoulombAtom.slaterTensor_orthonormalline 69 - lemma
OAI.CoulombAtom.slaterRaw_norm_sq_integralline 85 - def
OAI.CoulombAtom.slaterline 129 - lemma
OAI.CoulombAtom.memLp_slaterline 132 - lemma
OAI.CoulombAtom.slater_norm_sq_integralline 136