OAI/Analysis/CoulombIonization/Localization/GridPacketRadius.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.gridPacketRadius line 157
2. def OAI.CoulombAtom.packetKineticConstant line 158
3. def OAI.CoulombAtom.packetRepulsionConstant line 159
4. lemma OAI.CoulombAtom.packetKineticConstant_nonneg line 161
5. lemma OAI.CoulombAtom.packetRepulsionConstant_nonneg line 165
6. lemma OAI.CoulombAtom.gridPacketRadius_pos line 169
7. lemma OAI.CoulombAtom.gridPacketRadius_mul line 172
8. lemma OAI.CoulombAtom.gridPacketRadius_le line 178
9. lemma OAI.CoulombAtom.packetGrid_ball line 185
10. lemma OAI.CoulombAtom.packetGrid_repulsion line 191
11. theorem OAI.CoulombAtom.grid_packet_screening line 217