OAI/Analysis/CoulombIonization/Fermionic/SlaterRepulsion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CoulombAtom.slaterDirectDensity line 16
2. abbrev OAI.CoulombAtom.slaterExchangeDensity line 19
3. lemma OAI.CoulombAtom.slater_repulsion_spinSpace line 23
4. theorem OAI.CoulombAtom.slaterForm_repulsion line 42
5. lemma OAI.CoulombAtom.smooth_pair_integrable line 61
6. lemma OAI.CoulombAtom.smooth_nuclear_integrable line 68
7. lemma OAI.CoulombAtom.orbital_coulomb_product_integrable line 77
8. lemma OAI.CoulombAtom.slater_direct_coulomb_integrable line 112
9. lemma OAI.CoulombAtom.orbital_nuclear_integrable line 125
10. lemma OAI.CoulombAtom.memLp_potential_mul line 138
11. lemma OAI.CoulombAtom.slaterForm_nuclear line 148
12. theorem OAI.CoulombAtom.slaterForm_repulsion_le_direct line 182