OAI/Analysis/CoulombIonization/Fermionic/SlaterMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.pi_count_eq_count line 17
2. lemma OAI.CoulombAtom.spinSpace_measurePreserving line 25
3. lemma OAI.CoulombAtom.spinSpace_integral line 33
4. abbrev OAI.CoulombAtom.slaterParticleMeasure line 52
5. lemma OAI.CoulombAtom.compact_spinSpace line 55
6. lemma OAI.CoulombAtom.memLp_spinSpace line 62
7. lemma OAI.CoulombAtom.memLp_spatialOrbitalDerivative line 68
8. lemma OAI.CoulombAtom.slaterForm_mass line 76
9. theorem OAI.CoulombAtom.slaterForm_admissible line 86
10. theorem OAI.CoulombAtom.slaterForm_kinetic line 94