OAI/Analysis/CoulombIonization/RadialBounds/FreshRetainedMassBarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.compact_test_le_mass line 19
2. lemma OAI.CoulombAtom.masterCenteredKernel_amplitude line 42
3. def OAI.CoulombAtom.canonicalMasterAmplitude line 52
4. lemma OAI.CoulombAtom.canonicalMasterAmplitude_pos line 54
5. lemma OAI.CoulombAtom.canonicalMasterAmplitude_bound line 57
6. def OAI.CoulombAtom.freshHighThreshold line 74
7. lemma OAI.CoulombAtom.threshold_event_mean_le line 82
8. theorem OAI.CoulombAtom.TailTiltState.high_inverse_event line 91