OAI/Analysis/CoulombRadii/Packets/PacketDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.packetDensity line 93
2. lemma OAI.Coulomb.packetDensity_nonneg line 96
3. lemma OAI.Coulomb.packetDensity_measurable line 99
4. lemma OAI.Coulomb.packetDensity_integrable line 104
5. lemma OAI.Coulomb.schwartz_square_le line 111
6. lemma OAI.Coulomb.packetDensity_integrand_integrable line 116
7. lemma OAI.Coulomb.packetDensity_bound line 126
8. lemma OAI.Coulomb.packetDensity_support line 135
9. lemma OAI.Coulomb.complexWindow_tsupport line 149
10. lemma OAI.Coulomb.complexWindow_compactSupport line 157
11. lemma OAI.Coulomb.fermiPhase_center_mem line 163
12. lemma OAI.Coulomb.fermiPhase_momentum_bound line 171