OAI/Analysis/CoulombIonization/Variational/ComplexRealWeightPairing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.complex_real_weight_pairing line 38
2. lemma OAI.CoulombAtom.l2_real_weight_pairing line 45
3. lemma OAI.CoulombAtom.norm_div_sqrt_real_sq line 54
4. lemma OAI.CoulombAtom.FermionMultiplier.nuclear_weighted_pairing line 61
5. lemma OAI.CoulombAtom.FermionMultiplier.pair_weighted_pairing line 70
6. lemma OAI.CoulombAtom.binding_pairing_off line 79
7. lemma OAI.CoulombAtom.weighted_integrable line 102
8. lemma OAI.CoulombAtom.integral_weighted_add line 108
9. lemma OAI.CoulombAtom.integral_weighted_sub line 115
10. lemma OAI.CoulombAtom.integral_weighted_sum line 122
11. lemma OAI.CoulombAtom.integral_weighted_const_mul line 129
12. lemma OAI.CoulombAtom.integral_weighted_quantumDensity line 135