OAI/Analysis/CoulombIonization/FormDomain/UnboundedSpectrum.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.InUnboundedResolvent line 15
2. def OAI.CoulombAtom.unboundedSpectrum line 20
3. def OAI.CoulombAtom.inverseShift line 22
4. lemma OAI.CoulombAtom.vadd_graph_iff line 26
5. lemma OAI.CoulombAtom.inverseShift_graph line 41
6. lemma OAI.CoulombAtom.inverseShift_domain line 49
7. theorem OAI.CoulombAtom.inverseShift_selfAdjoint line 53
8. theorem OAI.CoulombAtom.inverseShift_resolvent_iff line 88
9. lemma OAI.CoulombAtom.unit_one_sub_smul_iff line 162
10. lemma OAI.CoulombAtom.inverseShift_spectrum_iff line 170
11. lemma OAI.CoulombAtom.inverseShift_spectrum_ne line 177
12. lemma OAI.CoulombAtom.inverseShift_real_spectrum_iff line 186
13. lemma OAI.CoulombAtom.inverseShift_spectrum_real line 193
14. theorem OAI.CoulombAtom.inverseShift_spectral_bottom line 204