OAI/Analysis/CoulombRadii/Localization/ShellIMS.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.imsShell line 15
2. lemma OAI.Coulomb.measurableSet_imsShell line 18
3. lemma OAI.Coulomb.radialCut_fderiv_zero_inner line 22
4. lemma OAI.Coulomb.radialCut_gradient_shell_bound line 37
5. theorem OAI.Coulomb.form_radial_labelCut_shell line 61
6. theorem OAI.NeutralAtom.fromH1_expectedPopulation line 95
7. lemma OAI.Coulomb.expectedPopulation_labelCut line 117