OAI/Analysis/CoulombIonization/Localization/PacketCloud.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.packetCloud line 155
2. lemma OAI.CoulombAtom.packetCloud_nonneg line 158
3. lemma OAI.CoulombAtom.packetCloud_integrable line 162
4. lemma OAI.CoulombAtom.packetCloud_memLp line 166
5. lemma OAI.CoulombAtom.packetCloud_exists line 170
6. lemma OAI.CoulombAtom.packetCloud_bound line 176
7. lemma OAI.CoulombAtom.packetCloud_support line 197
8. lemma OAI.CoulombAtom.packetCloud_potential_bound line 207
9. theorem OAI.CoulombAtom.packetPairEnergy_bound line 237
10. def OAI.CoulombAtom.packetGridPoint line 269
11. lemma OAI.CoulombAtom.packetGridPoint_apply line 272
12. lemma OAI.CoulombAtom.packetGridPoint_norm line 275
13. lemma OAI.CoulombAtom.packetGridPoint_separated line 292
14. lemma OAI.CoulombAtom.packetGrid_card line 313
15. def OAI.CoulombAtom.packetGrid line 315
16. lemma OAI.CoulombAtom.packetGrid_norm line 319
17. lemma OAI.CoulombAtom.packetGrid_separated line 326