OAI/Analysis/CoulombIonization/RadialBounds/BarrierStepGeometryBarrier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombBarrier.barrierGap line 19
  2. lemma OAI.CoulombBarrier.barrierGap_pos line 21
  3. lemma OAI.CoulombBarrier.outerBarrier_dyadic_difference line 25
  4. lemma OAI.CoulombBarrier.outerBarrier_dyadic_gap line 31
  5. lemma OAI.CoulombBarrier.shifted_old_above_new_barrier line 43
  6. lemma OAI.CoulombBarrier.cap_dominated_by_shift line 52
  7. def OAI.CoulombBarrier.shiftedCandidates line 61
  8. def OAI.CoulombBarrier.outwardOffset line 65
  9. lemma OAI.CoulombBarrier.shiftedCandidates_old_le line 70
  10. lemma OAI.CoulombBarrier.shiftedCandidates_continuous line 78
  11. lemma OAI.CoulombBarrier.outward_lower_overlap line 86
  12. lemma OAI.CoulombBarrier.outward_upper_overlap line 97
  13. lemma OAI.CoulombBarrier.DeterministicLocalLipschitz.ite line 123
  14. lemma OAI.CoulombBarrier.DeterministicLocalBound.ite line 135
  15. lemma OAI.CoulombBarrier.DeterministicLocalBound.max line 148
  16. lemma OAI.CoulombBarrier.shiftedCandidates_deterministicLip line 159
  17. lemma OAI.CoulombBarrier.shiftedCandidates_deterministicBound line 167
  18. lemma OAI.CoulombBarrier.shiftedCandidates_measurable line 179
  19. lemma OAI.CoulombBarrier.outwardOffset_measurable line 187
  20. lemma OAI.CoulombBarrier.outwardOffset_deterministicBound line 199