OAI/Analysis/CoulombIonization/FormDomain/BindingSums.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.graphNuclearSum line 23
2. lemma OAI.CoulombAtom.graphNuclearSum_bound line 26
3. lemma OAI.CoulombAtom.binding_nuclear_sum_bound line 47
4. lemma OAI.CoulombAtom.sum_pair_tail_bound line 69
5. lemma OAI.CoulombAtom.binding_pair_sum_bound line 101
6. lemma OAI.CoulombAtom.FermionMultiplier.mass_bound line 148
7. lemma OAI.CoulombAtom.FermionMultiplier.kinetic_bound line 155
8. theorem OAI.CoulombAtom.FermionMultiplier.graph_bound line 173
9. theorem OAI.CoulombAtom.quantum_approximate_multiplier line 188