OAI/Analysis/CoulombIonization/Variational/BindingPairApproxIntegral.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.bindingPairApprox_integral_le line 47
2. lemma OAI.CoulombAtom.bindingPairApprox_integral_le_rev line 62
3. lemma OAI.CoulombAtom.sum_pair_bound line 76
4. lemma OAI.CoulombAtom.sum_excluding_const line 86
5. lemma OAI.CoulombAtom.integral_weighted_deletedDensity line 99
6. lemma OAI.CoulombAtom.binding_total_kinetic_lower line 141
7. lemma OAI.CoulombAtom.integral_weighted_quantumDensity_ordered line 166
8. lemma OAI.CoulombAtom.FermionMultiplier.density_weighted_identity line 184
9. lemma OAI.CoulombAtom.FermionMultiplier.operator_weighted_pairing line 198
10. lemma OAI.CoulombAtom.weighted_form_algebra line 209
11. lemma OAI.CoulombAtom.FermionMultiplier.density_weighted_sum line 213
12. lemma OAI.CoulombAtom.FermionMultiplier.form_weighted_identity line 227