OAI/Analysis/CoulombIonization/ThomasFermi/TfDilation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.tfDilation line 46
  2. lemma OAI.CoulombAtom.space_finrank line 52
  3. lemma OAI.CoulombAtom.product_finrank line 54
  4. lemma OAI.CoulombAtom.tfDilation_mass line 57
  5. lemma OAI.CoulombAtom.tfDilation_kinetic line 64
  6. lemma OAI.CoulombAtom.tfDilation_nuclear line 71
  7. lemma OAI.CoulombAtom.tfDilation_direct line 76
  8. lemma OAI.CoulombAtom.tfDilation_admissible line 82
  9. lemma OAI.CoulombAtom.tfDilation_functional line 100
  10. lemma OAI.CoulombAtom.tfDilation_inv line 117
  11. theorem OAI.CoulombAtom.tfEnergy_scaling line 122
  12. theorem OAI.CoulombAtom.tfIonization_scaling line 142
  13. theorem OAI.CoulombAtom.tfCharacterization_of_unit_limit line 167
  14. lemma OAI.CoulombAnalysis.tfKinetic_pos line 183
  15. lemma OAI.CoulombAnalysis.tfExtension_nonneg line 187
  16. lemma OAI.CoulombAnalysis.tfExtension_kinetic line 195
  17. lemma OAI.CoulombAnalysis.tfExtension_nuclear line 201
  18. lemma OAI.CoulombAnalysis.tfExtension_kinetic_integrable line 206
  19. lemma OAI.CoulombAnalysis.tfExtension_nuclear_integrable line 211
  20. lemma OAI.CoulombAnalysis.tfExtension_admissible line 217
  21. lemma OAI.CoulombAnalysis.tfExtension_functional line 223
  22. lemma OAI.CoulombAnalysis.tfAdmissible_memLp line 243
  23. lemma OAI.CoulombAnalysis.tfAdmissible_truncate line 250
  24. lemma OAI.CoulombAnalysis.tfFunctional_congr_ae line 264
  25. lemma OAI.CoulombAnalysis.tfIndicator_direct line 275
  26. lemma OAI.CoulombAnalysis.tfIndicator_kinetic line 282
  27. lemma OAI.CoulombAnalysis.tfIndicator_linear line 288
  28. lemma OAI.CoulombAnalysis.tfPriced_truncate_le line 294
  29. theorem OAI.CoulombAnalysis.tf_unit_price_exists_minimizer line 344