OAI/Analysis/CoulombRadii/SpectralTheory/BindingBump.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.bindingBump line 13
  2. def OAI.NeutralAtom.bindingCutoff line 16
  3. theorem OAI.NeutralAtom.bindingCutoff_smooth line 19
  4. theorem OAI.NeutralAtom.bindingCutoff_symmetric line 22
  5. theorem OAI.NeutralAtom.bindingCutoff_nonneg line 26
  6. theorem OAI.NeutralAtom.bindingCutoff_le_one line 29
  7. theorem OAI.NeutralAtom.bindingCutoff_eq_one line 32
  8. theorem OAI.NeutralAtom.bindingCutoff_eq_zero line 40
  9. theorem OAI.NeutralAtom.bindingCutoff_compact line 49
  10. theorem OAI.NeutralAtom.bindingCutoff_derivative_bounded line 55
  11. def OAI.NeutralAtom.bindingScale line 61
  12. def OAI.NeutralAtom.expandingCutoff line 63
  13. theorem OAI.NeutralAtom.bindingScale_pos line 66
  14. theorem OAI.NeutralAtom.bindingScale_le_one line 69
  15. theorem OAI.NeutralAtom.bindingScale_tendsto line 74
  16. theorem OAI.NeutralAtom.expandingCutoff_smooth line 78
  17. theorem OAI.NeutralAtom.expandingCutoff_nonneg line 82
  18. theorem OAI.NeutralAtom.expandingCutoff_le_one line 85
  19. theorem OAI.NeutralAtom.expandingCutoff_fderiv line 88
  20. theorem OAI.NeutralAtom.expandingCutoff_multiplier line 98
  21. theorem OAI.NeutralAtom.expandingCutoff_tendsto line 117
  22. theorem OAI.NeutralAtom.expandingCutoff_fderiv_tendsto line 123
  23. theorem OAI.NeutralAtom.expandingCutoff_eq_zero line 130
  24. theorem OAI.NeutralAtom.expandingCutoff_derivative_uniform_bound line 138
  25. theorem OAI.NeutralAtom.integral_expandingCutoff_sq_tendsto line 151
  26. theorem OAI.NeutralAtom.normSquared_cutoff_tendsto line 167
  27. theorem OAI.NeutralAtom.kinetic_cutoff_tendsto line 175
  28. theorem OAI.NeutralAtom.energy_cutoff_tendsto line 204
  29. theorem OAI.NeutralAtom.expandingCutoff_fderiv_eq_zero line 220
  30. theorem OAI.NeutralAtom.FormDomain.exists_compact_approximation line 227
  31. theorem OAI.NeutralAtom.memLp_two_real_tensor line 264
  32. def OAI.NeutralAtom.WeakDirectionalDerivative line 281
  33. theorem OAI.NeutralAtom.compact_support_partial_right line 289
  34. theorem OAI.NeutralAtom.compact_support_partial_left line 303
  35. theorem OAI.NeutralAtom.fderiv_partial_right line 316
  36. theorem OAI.NeutralAtom.fderiv_partial_left line 326
  37. theorem OAI.NeutralAtom.WeakDirectionalDerivative.tensor_right line 333
  38. theorem OAI.NeutralAtom.smooth_tensor_weak_left line 359
  39. theorem OAI.NeutralAtom.WeakDirectionalDerivative.comp_equiv line 408