OAI/Analysis/CoulombIonization/RadialBounds/BarrierSmoothMaxBarrier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombBarrier.second_fderiv_scalar_comp line 17
  2. lemma OAI.CoulombBarrier.laplacian_scalar_comp_lower line 46
  3. def OAI.CoulombBarrier.smoothPositive line 59
  4. lemma OAI.CoulombBarrier.smoothPositive_contDiff line 61
  5. lemma OAI.CoulombBarrier.smoothRoot_hasDerivAt line 66
  6. lemma OAI.CoulombBarrier.smoothPositive_deriv line 77
  7. lemma OAI.CoulombBarrier.smoothPositive_deriv_bounds line 82
  8. lemma OAI.CoulombBarrier.smoothPositive_second_nonneg line 94
  9. def OAI.CoulombBarrier.smoothMaximum line 113
  10. lemma OAI.CoulombBarrier.smoothMaximum_contDiff line 116
  11. theorem OAI.CoulombBarrier.smoothMaximum_laplacian_lower line 121
  12. lemma OAI.CoulombBarrier.smoothPositive_bounds line 138
  13. lemma OAI.CoulombBarrier.smoothMaximum_bounds line 156
  14. lemma OAI.CoulombBarrier.smoothMaximum_norm_bound line 168
  15. lemma OAI.CoulombBarrier.smoothMaximum_tendsto line 179