OAI/Analysis/CoulombRadii/SpectralTheory/StrictBinding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.binding_cost_tendsto line 12
2. lemma OAI.Coulomb.strictly_bound_sequence_tight line 18
3. lemma OAI.Coulomb.atom_strict_binding_attained line 41
4. lemma OAI.NeutralAtom.integral_first_weighted_tensor line 67
5. lemma OAI.NeutralAtom.weighted_normSquared_insert_first line 81
6. lemma OAI.NeutralAtom.distantPacket_outer_zero line 90
7. lemma OAI.NeutralAtom.distantPacket_attraction line 100
8. lemma OAI.NeutralAtom.onePacket_domain line 118
9. lemma OAI.NeutralAtom.onePacket_energy line 139
10. lemma OAI.NeutralAtom.sectorEnergy_one_neg line 158