OAI/Analysis/CoulombIonization/RadialBounds/SpatialCapSubmeanBarrier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.capBandStatistic line 17
2. lemma OAI.CoulombAtom.cap_interior_ball_subset line 21
3. lemma OAI.CoulombAtom.scalar_cap_excess_mono line 31
4. lemma OAI.CoulombAtom.submean_le_capBandStatistic line 40
5. theorem OAI.CoulombAtom.capBandStatistic_simultaneous_cap line 79
6. lemma OAI.CoulombAtom.capBandStatistic_integrable line 102
7. lemma OAI.CoulombAtom.capBandStatistic_nonneg line 109
8. lemma OAI.CoulombAtom.capBandStatistic_expectation line 114
9. theorem OAI.CoulombAtom.capBandStatistic_failure_probability line 146