OAI/Analysis/CoulombIonization/Localization/FermiDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.smearedPacketDensity line 18
2. lemma OAI.CoulombAtom.coherentDensity_fermi line 21
3. lemma OAI.CoulombAtom.smearedPacketDensity_nonneg line 36
4. lemma OAI.CoulombAtom.smearedPacketDensity_continuous line 39
5. lemma OAI.CoulombAtom.smearedPacketDensity_compact line 49
6. lemma OAI.CoulombAtom.smearedPacketDensity_mass line 63
7. lemma OAI.CoulombAtom.coulomb_double_eq_potential line 80
8. lemma OAI.CoulombAtom.coulomb_potential_pair_integrable line 88
9. lemma OAI.CoulombAtom.coulomb_potential_pair_comm line 93
10. lemma OAI.CoulombAtom.coulomb_direct_le_of_potential_le line 108
11. lemma OAI.CoulombAtom.square_compact line 132
12. lemma OAI.CoulombAtom.smearedPacketDensity_direct_le line 135