OAI/Analysis/CoulombIonization/Ionization/IteratedReduction.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CoulombAtom.uniform_tail_of_sequential_jointline 15 - lemma
OAI.CoulombAtom.eventual_Z_band_of_jointline 38 - lemma
OAI.CoulombAtom.liminf_limsup_bounded_by_eventualline 55 - theorem
OAI.CoulombAtom.iteratedLimits_of_jointLimitline 63 - lemma
OAI.CoulombAtom.positive_map_eq_zero_of_innerline 108 - theorem
OAI.CoulombAtom.ground_form_equationline 134 - lemma
OAI.CoulombAtom.complex_ims_identityline 168