OAI/Analysis/CoulombIonization/ThomasFermi/TfBallFunctionalConvex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAnalysis.tfBallFunctional_convex line 71
  2. lemma OAI.CoulombAnalysis.tfAdmissible_extension line 93
  3. lemma OAI.CoulombAnalysis.tfExtension_add_smul line 102
  4. lemma OAI.CoulombAnalysis.tf_compact_mix line 112
  5. lemma OAI.CoulombAnalysis.tf_compact_mass_exists line 142
  6. lemma OAI.CoulombAnalysis.tfEnergy_class_nonempty line 178
  7. lemma OAI.CoulombAnalysis.tfEnergy_class_bddBelow line 183
  8. lemma OAI.CoulombAnalysis.tfEnergy_le_trial line 191
  9. def OAI.CoulombAnalysis.tfPriceValue line 195
  10. def OAI.CoulombAnalysis.tfPriceDeficit line 200
  11. lemma OAI.CoulombAnalysis.tfPriceDeficit_eq line 202
  12. lemma OAI.CoulombAnalysis.tfPriceValue_eq line 206
  13. lemma OAI.CoulombAnalysis.tfPriceValue_le_trial line 210
  14. lemma OAI.CoulombAnalysis.tfPriceValue_le_energy line 217
  15. lemma OAI.CoulombAnalysis.tfPriceValue_secant line 225
  16. lemma OAI.CoulombAnalysis.tfPriceDeficit_zero_tendsto line 231
  17. lemma OAI.CoulombAnalysis.tfPriceValue_zero_tendsto line 248
  18. lemma OAI.CoulombAnalysis.tfPriceValue_zero_bounds line 290