OAI/Analysis/CoulombRadii/ThomasFermi/ScaledProfile.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.scaledProfile line 15
  2. theorem OAI.NeutralAtom.continuousOn_scaledProfile line 17
  3. theorem OAI.NeutralAtom.scaled_reaction line 21
  4. theorem OAI.NeutralAtom.penalized_max_reaction_bound line 29
  5. theorem OAI.NeutralAtom.penalized_min_reaction_bound line 62
  6. theorem OAI.NeutralAtom.exists_approximate_penalized_max line 95
  7. theorem OAI.NeutralAtom.exists_approximate_penalized_min line 114
  8. theorem OAI.NeutralAtom.reaction_le_at_supremum line 133
  9. theorem OAI.NeutralAtom.reaction_ge_at_infimum line 157
  10. theorem OAI.NeutralAtom.scalar_upper_contact line 181
  11. theorem OAI.NeutralAtom.scalar_lower_contact line 191
  12. theorem OAI.NeutralAtom.weak_sommerfeld_rigidity line 202
  13. theorem OAI.NeutralAtom.WeakLaplacianLower.add_smooth line 245
  14. theorem OAI.NeutralAtom.weak_maximum_principle_closedBall line 278
  15. def OAI.NeutralAtom.kTF line 333
  16. def OAI.NeutralAtom.aTF line 334
  17. theorem OAI.NeutralAtom.kTF_pos line 336
  18. theorem OAI.NeutralAtom.aTF_pos line 338
  19. theorem OAI.NeutralAtom.rpow_three_halves line 343
  20. theorem OAI.NeutralAtom.aTF_value line 348
  21. theorem OAI.NeutralAtom.profile_coefficient line 361
  22. theorem OAI.NeutralAtom.weak_sommerfeld_rigidity_exact line 371
  23. def OAI.NeutralAtom.WeakLaplacianGE line 390
  24. theorem OAI.NeutralAtom.WeakLaplacianGE.lower_on line 394
  25. theorem OAI.NeutralAtom.weak_comparison_closedBall line 410