OAI/Analysis/CoulombIonization/Variational/CoherentDensity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.coherentDensity line 16
2. lemma OAI.CoulombAtom.coherentDensity_nonneg line 19
3. lemma OAI.CoulombAtom.coherentDensity_continuous line 23
4. lemma OAI.CoulombAtom.coherentDensity_zero_outside line 36
5. lemma OAI.CoulombAtom.coherentDensity_compact line 45
6. lemma OAI.CoulombAtom.coherentDensity_integrable line 53
7. lemma OAI.CoulombAtom.coherentPacket_sq_integrable line 60
8. lemma OAI.CoulombAtom.coherentPacket_mass line 77
9. lemma OAI.CoulombAtom.coherentDensity_mass line 84
10. lemma OAI.CoulombAtom.coherentPositiveWeight_hasSum line 97
11. lemma OAI.CoulombAtom.coherentOrbital_mass line 106