OAI/Analysis/CoulombIonization/RadialBounds/BarrierInitialInvariantBarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CoulombBarrier.IsNuclearBarrier line 21
2. lemma OAI.CoulombBarrier.IsNuclearBarrier.locallyLipschitz_offset line 39
3. lemma OAI.CoulombBarrier.initial_error_mass_power line 44
4. theorem OAI.CoulombBarrier.initial_barrier_invariant line 61
5. lemma OAI.CoulombBarrier.nonneg_bounded_deterministicBound line 116
6. lemma OAI.CoulombBarrier.nonneg_bounded_locallyIntegrable line 121
7. lemma OAI.CoulombBarrier.expected_mass_add line 125
8. theorem OAI.CoulombBarrier.outward_barrier_invariant line 138