OAI/Analysis/CoulombIonization/FormDomain/Restriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.restrictWeakGraph line 35
2. def OAI.CoulombAtom.SmoothMultiplier.restrict line 39
3. lemma OAI.CoulombAtom.SmoothMultiplier.restrict_apply line 47
4. lemma OAI.CoulombAtom.SmoothMultiplier.projected_kinetic_nonneg line 55
5. lemma OAI.CoulombAtom.lineDeriv_binding_coordinate line 68
6. def OAI.CoulombAtom.bindingMultiplier line 83
7. lemma OAI.CoulombAtom.bindingMultiplier_kinetic_nonneg line 94