OAI/Analysis/CoulombIonization/Variational/Weighted.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.SmoothMultiplier.weighted_kinetic_nonneg line 31
2. def OAI.CoulombAtom.bindingWeight line 76
3. def OAI.CoulombAtom.bindingRoot line 79
4. lemma OAI.CoulombAtom.bindingWeight_pos line 81
5. lemma OAI.CoulombAtom.bindingWeight_le line 87
6. lemma OAI.CoulombAtom.bindingWeight_le_radius line 94
7. lemma OAI.CoulombAtom.bindingRoot_sq line 101
8. lemma OAI.CoulombAtom.bindingRoot_pos line 105
9. lemma OAI.CoulombAtom.bindingRoot_bound line 108
10. lemma OAI.CoulombAtom.bindingRoot_smooth line 113
11. lemma OAI.CoulombAtom.bindingRoot_derivative line 122
12. lemma OAI.CoulombAtom.bindingRoot_gradient_bound line 152
13. lemma OAI.CoulombAtom.bindingRoot_hardy_control line 177