OAI/Analysis/CoulombRadii/ThomasFermi/TFInterior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.tfPotential_nonneg_of_nonneg line 19
2. lemma OAI.Coulomb.tfDensity_bound_of_minimizes line 25
3. lemma OAI.Coulomb.tfPotential_continuous_of_minimizes line 44
4. lemma OAI.Coulomb.tfScreened_weak_equation line 68
5. theorem OAI.Coulomb.tfScreened_interior_upper line 108
6. def OAI.Coulomb.tfInteriorConstant line 125
7. lemma OAI.Coulomb.tfInteriorConstant_nonneg line 129
8. lemma OAI.Coulomb.tfScreened_three_quarters line 132
9. lemma OAI.Coulomb.tfDensity_interior_bound line 160