OAI/Analysis/CoulombRadii/LimitTheory/TailFinish.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NeutralAtom.Admissible.charge_tendsto line 13
2. theorem OAI.NeutralAtom.expected_exterior_of_raw_annuli line 24
3. theorem OAI.NeutralAtom.quantum_profile_packet_limit line 68