OAI/Analysis/CoulombRadii/Packets/WindowCoulomb.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.window_coulomb_eq line 111
2. lemma OAI.Coulomb.window_coulomb_bound line 120
3. lemma OAI.Coulomb.packetDensity_coulomb_prod_integrable line 127
4. lemma OAI.Coulomb.packetDensity_coulomb_integral line 155
5. lemma OAI.Coulomb.packetDensity_coulomb_eq line 169
6. lemma OAI.Coulomb.separated_density_coulomb_integrable line 183
7. lemma OAI.Coulomb.coreCoulombPotential_packet_eq line 195
8. lemma OAI.Coulomb.separated_density_nuclear_integrable line 217
9. lemma OAI.Coulomb.attraction_packet_eq line 232
10. lemma OAI.Coulomb.coreScreenedField_packet_eq line 256
11. theorem OAI.Coulomb.source_free_trial_in_hole line 272