OAI/Analysis/CoulombIonization/Localization/ObservedAnnularCountBarrier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.observedAnnularCount line 23
2. lemma OAI.CoulombAtom.observedAnnularCount_information_measurable line 27
3. lemma OAI.CoulombAtom.observed_annular_count_le_raw line 35
4. lemma OAI.CoulombAtom.rawAnnularMoment_eq_integral line 52
5. lemma OAI.CoulombAtom.rawAnnularCount_sq_integrable line 57
6. lemma OAI.CoulombAtom.event_raw_annular_count_lower line 63
7. lemma OAI.CoulombAtom.annularOffsetMass_one_small line 93
8. theorem OAI.CoulombAtom.exists_actual_priced_moment_constant line 108
9. theorem OAI.CoulombAtom.actual_original_posterior_moment line 128