OAI/Analysis/CoulombIonization/Variational/CoherentOrbitals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.coherentOperator_synthesis line 17
2. def OAI.CoulombAtom.coherentOrbital line 27
3. lemma OAI.CoulombAtom.coherentOrbital_smooth line 32
4. lemma OAI.CoulombAtom.coherentOrbital_zero_outside line 41
5. lemma OAI.CoulombAtom.coherentOrbital_compact line 48
6. lemma OAI.CoulombAtom.coherentOrbital_memLp line 54
7. lemma OAI.CoulombAtom.coherentOrbital_toLp line 61
8. lemma OAI.CoulombAtom.coherentOrbital_ae line 77
9. lemma OAI.CoulombAtom.coherentOrbital_inner line 85