OAI/Analysis/CoulombIonization/Localization/PacketInsert.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.packetInsert line 140
2. lemma OAI.CoulombAtom.packetInsert_sobolev line 145
3. lemma OAI.CoulombAtom.packetInsert_avoids line 151
4. lemma OAI.CoulombAtom.packetInsert_disjoint line 161
5. lemma OAI.CoulombAtom.packetInsert_mass line 172
6. lemma OAI.CoulombAtom.packetInsert_field line 188
7. def OAI.CoulombAtom.packetPairEnergy line 215
8. def OAI.CoulombAtom.packetScreenedSum line 218
9. lemma OAI.CoulombAtom.packetInsert_energy line 221
10. theorem OAI.CoulombAtom.many_packet_screening line 249