OAI/Analysis/CoulombRadii/Localization/ShellChoice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.localCountSecondMoment_cover line 13
2. lemma OAI.Coulomb.localCount_disjoint_sum_le line 30
3. lemma OAI.Coulomb.localCountSecondMoment_disjoint_sum_le line 54
4. def OAI.Coulomb.deletedShell line 72
5. lemma OAI.Coulomb.deletedShell_measurable line 74
6. lemma OAI.Coulomb.deletedShell_disjoint line 79
7. theorem OAI.Coulomb.exists_deletedShell_small line 87