OAI/Analysis/CoulombRadii/Localization/AnnularCut.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.annularAngle line 12
2. def OAI.Coulomb.annularCut line 14
3. lemma OAI.Coulomb.annularAngle_smooth line 17
4. lemma OAI.Coulomb.annularCut_smooth line 20
5. lemma OAI.Coulomb.annularCut_partition line 26
6. lemma OAI.Coulomb.cutAngle_inner line 29
7. lemma OAI.Coulomb.cutAngle_outer line 36
8. lemma OAI.Coulomb.annularCut_core_zero line 43
9. lemma OAI.Coulomb.annularCut_out_zero line 49
10. lemma OAI.Coulomb.cutAngle_derivative_bound line 61
11. lemma OAI.Coulomb.annularAngle_derivative_bound line 71
12. lemma OAI.Coulomb.annularCut_derivative_bound line 85