OAI/Analysis/CoulombRadii/ThomasFermi/AtomicThinCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.atomicPatchCountFactor line 14
2. lemma OAI.Coulomb.atomicPatchCountFactor_nonneg line 15
3. lemma OAI.Coulomb.atomicPatch_secondMoment line 17
4. lemma OAI.Coulomb.exists_atomic_deletedShell line 47
5. def OAI.Coulomb.thinReserveFactor line 65
6. lemma OAI.Coulomb.thinReserveFactor_ge_one line 66
7. lemma OAI.Coulomb.thinReserveFactor_nonneg line 67
8. lemma OAI.Coulomb.thinIMS_budget line 69