OAI/Analysis/CoulombRadii/Packets/ComplexWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.complexWindow line 81
2. lemma OAI.Coulomb.complexWindow_apply line 83
3. lemma OAI.Coulomb.packetState_real_derivative_norm line 86
4. lemma OAI.Coulomb.real_schwartz_derivative_square_integrable line 95
5. lemma OAI.Coulomb.packetState_real_kinetic_integral line 100
6. lemma OAI.Coulomb.packetState_fourier_joint_square_integrable line 114
7. lemma OAI.Coulomb.packetState_real_weighted_joint_integrable line 132