OAI/Analysis/CoulombIonization/RadialBounds/OwnProbabilityRareCapBarrier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.tinyProbabilityFloor_le_eighty line 21
2. lemma OAI.CoulombAtom.originalQueryField_info_measurable line 25
3. theorem OAI.CoulombAtom.OwnProbabilityTailTiltState.rare_cap_event line 33
4. lemma OAI.CoulombAtom.integral_positive_excess_le line 63
5. theorem OAI.CoulombAtom.actual_cap_excess_eventually line 92
6. theorem OAI.CoulombAtom.actual_cap_excess_uniform_eventually line 143