OAI/Analysis/CoulombRadii/Propagation/SmoothMaximum.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.softAbs line 13
  2. def OAI.NeutralAtom.softSlope line 14
  3. def OAI.NeutralAtom.softWeight line 15
  4. def OAI.NeutralAtom.softPlus line 16
  5. def OAI.NeutralAtom.softMax line 17
  6. lemma OAI.NeutralAtom.softAbs_pos line 19
  7. lemma OAI.NeutralAtom.softAbs_sq line 23
  8. lemma OAI.NeutralAtom.abs_le_softAbs line 26
  9. lemma OAI.NeutralAtom.softWeight_bounds line 30
  10. lemma OAI.NeutralAtom.softAbs_hasDerivAt line 37
  11. lemma OAI.NeutralAtom.softSlope_hasDerivAt line 46
  12. lemma OAI.NeutralAtom.softPlus_hasDerivAt line 58
  13. lemma OAI.NeutralAtom.softWeight_hasDerivAt line 62
  14. lemma OAI.NeutralAtom.contDiff_softAbs line 69
  15. lemma OAI.NeutralAtom.contDiff_softPlus line 74
  16. lemma OAI.NeutralAtom.contDiff_softMax line 77
  17. lemma OAI.NeutralAtom.second_deriv_comp_scalar line 82
  18. lemma OAI.NeutralAtom.second_deriv_softPlus line 100
  19. lemma OAI.NeutralAtom.coordinateLaplacian_comp_scalar line 106
  20. lemma OAI.NeutralAtom.coordinateLaplacian_softMax_lower line 117
  21. lemma OAI.NeutralAtom.softAbs_le line 145
  22. lemma OAI.NeutralAtom.softMax_zero line 150
  23. lemma OAI.NeutralAtom.softMax_bounds line 159
  24. lemma OAI.NeutralAtom.softMax_abs_le line 169
  25. lemma OAI.NeutralAtom.softMax_tendsto line 178
  26. lemma OAI.NeutralAtom.softWeight_tendsto_of_lt line 184
  27. lemma OAI.NeutralAtom.softWeight_tendsto_of_gt line 195
  28. lemma OAI.NeutralAtom.convex_pair_bounds line 207
  29. lemma OAI.NeutralAtom.softWeight_response_tendsto line 216