OAI/Analysis/CoulombIonization/ThomasFermi/TfCenteredPrice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.tfPriceDeficit_tendsto line 74
2. lemma OAI.CoulombAnalysis.tfPriceDeficit_of_nonpos line 81
3. def OAI.CoulombAnalysis.tfCenteredPrice line 86
4. lemma OAI.CoulombAnalysis.tfCenteredPrice_secants line 88
5. lemma OAI.CoulombAnalysis.tfCenteredPrice_bounds line 99
6. theorem OAI.CoulombAnalysis.tf_priced_energy_limits line 105
7. lemma OAI.CoulombAnalysis.tfIonization_le_priced_max line 121