OAI/Analysis/CoulombIonization/RadialBounds/BarrierInitialLipschitzBarrier.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombBarrier.bounded_density_potential_locallyLipschitz line 19
  2. lemma OAI.CoulombBarrier.initialOffset_locallyLipschitz line 36
  3. lemma OAI.CoulombBarrier.locallyLipschitz_comp_contDiffAt line 45
  4. lemma OAI.CoulombBarrier.outerOffset_locallyLipschitz line 54
  5. lemma OAI.CoulombBarrier.lipschitz_nhds_congr line 65
  6. lemma OAI.CoulombBarrier.cutMaximum_locallyLipschitz line 75
  7. lemma OAI.CoulombBarrier.initializedOffset_locallyLipschitz line 97
  8. def OAI.CoulombBarrier.DeterministicLocalLipschitz line 128
  9. lemma OAI.CoulombBarrier.DeterministicLocalLipschitz.locallyLipschitz line 131
  10. lemma OAI.CoulombBarrier.deterministicLip_spatial line 137
  11. lemma OAI.CoulombBarrier.DeterministicLocalLipschitz.neg line 143
  12. lemma OAI.CoulombBarrier.DeterministicLocalLipschitz.add line 149
  13. lemma OAI.CoulombBarrier.DeterministicLocalLipschitz.sub line 158
  14. lemma OAI.CoulombBarrier.DeterministicLocalLipschitz.max line 163
  15. lemma OAI.CoulombBarrier.deterministicLip_local_congr line 173
  16. lemma OAI.CoulombBarrier.cutMaximum_deterministicLip line 183
  17. lemma OAI.CoulombBarrier.bounded_density_potential_deterministicLip line 205
  18. lemma OAI.CoulombBarrier.average_locallyLipschitz line 224
  19. lemma OAI.CoulombBarrier.initialOffset_deterministicLip line 241
  20. lemma OAI.CoulombBarrier.initializedOffset_deterministicLip line 252
  21. lemma OAI.CoulombBarrier.conditionalField_deterministicLip line 279