OAI/Analysis/CoulombRadii/Localization/ExteriorCut.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.exteriorCut line 13
2. lemma OAI.Coulomb.exteriorCut_smooth line 16
3. lemma OAI.Coulomb.exteriorCut_partition line 20
4. lemma OAI.Coulomb.exteriorCut_derivative_bound line 24
5. lemma OAI.Coulomb.exteriorCut_out_zero line 29
6. lemma OAI.Coulomb.exteriorCut_core_zero line 33
7. lemma OAI.Coulomb.exteriorCut_gradient_sum line 37
8. lemma OAI.Coulomb.form_exterior_labelCut_shell line 43
9. theorem OAI.Coulomb.exists_atomic_exterior_IMS_bound line 52