OAI/Analysis/CoulombRadii/FormDomain/CoreKinetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.potentialForm_coreSlice_parameter_ae line 123
2. lemma OAI.Coulomb.potentialForm_coreSlice_parameter_integrable line 130
3. lemma OAI.Coulomb.integral_potentialForm_coreSlice_parameter line 148
4. lemma OAI.Coulomb.potentialForm_const line 188
5. lemma OAI.Coulomb.H1Vector.outer_nuclear_integrable line 192
6. lemma OAI.Coulomb.H1Vector.outer_pair_integrable line 204
7. lemma OAI.Coulomb.H1Vector.cross_integrable line 218
8. def OAI.Coulomb.coreKinetic line 231
9. def OAI.Coulomb.outerKinetic line 234
10. lemma OAI.Coulomb.kinetic_split line 238
11. lemma OAI.Coulomb.nuclearEnergy_split line 244
12. lemma OAI.Coulomb.pairEnergy_split line 258
13. lemma OAI.Coulomb.form_normalized_weight line 280
14. lemma OAI.Coulomb.form_coreSlice_integrable line 288
15. lemma OAI.Coulomb.conditional_core_form_identity line 296