OAI/Analysis/CoulombRadii/ThomasFermi/PacketFrame.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.packetFrame line 78
2. lemma OAI.Coulomb.packetFrame_schwartz_quadratic_le line 82
3. lemma OAI.Coulomb.packetFrame_quadratic_le line 96
4. lemma OAI.Coulomb.packetFrame_positive line 111
5. lemma OAI.Coulomb.packetFrame_complement_positive line 116
6. lemma OAI.Coulomb.packetFrame_compact line 125
7. lemma OAI.Coulomb.packetFrame_spectral_trace line 129