OAI/Analysis/CoulombIonization/ThomasFermi/TfEulerDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.tfAdmissible_congr line 60
2. lemma OAI.CoulombAnalysis.tfPotential_congr line 72
3. lemma OAI.CoulombAnalysis.tfField_congr line 76
4. lemma OAI.CoulombAnalysis.tfField_continuousAt line 79
5. def OAI.CoulombAnalysis.tfEulerDensity line 84
6. lemma OAI.CoulombAnalysis.tfEulerDensity_nonneg line 87
7. lemma OAI.CoulombAnalysis.tfEulerDensity_continuousAt line 92
8. lemma OAI.CoulombAnalysis.tfEulerDensity_support line 96
9. theorem OAI.CoulombAnalysis.tf_unit_price_exists_regular line 103