OAI/Analysis/CoulombRadii/Screening/CoreCount.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.localCount_core_le line 13
2. lemma OAI.Coulomb.localCount_le_core line 22
3. lemma OAI.Coulomb.PartlySupported.core_population line 34
4. def OAI.Coulomb.positiveInnerDeficit line 53
5. lemma OAI.Coulomb.positiveInnerDeficit_measurable line 56
6. lemma OAI.Coulomb.positiveInnerDeficit_nonneg line 60
7. lemma OAI.Coulomb.positiveInnerDeficit_le line 63
8. lemma OAI.Coulomb.PartlySupported.deficit_moment line 66
9. def OAI.Coulomb.RecordedEnsemble.coreMean line 93
10. def OAI.Coulomb.RecordedEnsemble.coreDeficitMoment line 94
11. def OAI.Coulomb.RecordedEnsemble.favorableMass line 96
12. lemma OAI.Coulomb.RecordedEnsemble.coreMean_le_population line 99
13. lemma OAI.Coulomb.RecordedEnsemble.coreDeficitMoment_le_raw line 105
14. lemma OAI.Coulomb.RecordedEnsemble.favorableMass_of_core_moments line 121