OAI/Analysis/CoulombIonization/RadialBounds/ExteriorScreenNumerics.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.exteriorGradientConstant line 14
  2. lemma OAI.CoulombAtom.exteriorGradientConstant_nonneg line 15
  3. def OAI.CoulombAtom.actualScreenRadius line 17
  4. lemma OAI.CoulombAtom.actualScreenRadius_ge line 18
  5. lemma OAI.CoulombAtom.actualScreenRadius_ge16 line 19
  6. lemma OAI.CoulombAtom.actualScreenRadius_pos line 20
  7. lemma OAI.CoulombAtom.actualScreenRadius_square line 21
  8. lemma OAI.CoulombAtom.exterior_price_gradient_absorb line 28
  9. lemma OAI.CoulombAtom.annularOffsetMass_one_small_two line 37
  10. lemma OAI.CoulombAtom.exterior_bound_scale line 47
  11. def OAI.CoulombAtom.actualScreenConstant line 65
  12. lemma OAI.CoulombAtom.actualScreenConstant_nonneg line 68
  13. lemma OAI.CoulombAtom.exists_own_state_exterior_number_succ line 75
  14. lemma OAI.CoulombAtom.exists_own_state_exterior_number line 96
  15. def OAI.CoulombBarrier.selectedTailRadius line 119
  16. theorem OAI.CoulombBarrier.selected_data_of_events line 121