OAI/Analysis/CoulombRadii/ThomasFermi/TFOscillation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.tfPotential_eq_density line 20
2. lemma OAI.Coulomb.tfPotential_ballCloud_integrable line 28
3. lemma OAI.Coulomb.tfPotential_ballCloud_le line 35
4. lemma OAI.Coulomb.tfScreened_ballCloud_submean line 44
5. lemma OAI.Coulomb.tfEulerDensity_of_cap line 54
6. theorem OAI.Coulomb.tfScreened_interior_oscillation line 70
7. def OAI.Coulomb.patchTFScreenedField line 131
8. theorem OAI.Coulomb.exists_patch_TF_oscillation line 137