OAI/Analysis/CoulombRadii/Packets/PacketWindowed.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.packetWindowed line 75
2. lemma OAI.Coulomb.packetWindowed_apply line 78
3. def OAI.Coulomb.packetAnalysis line 84
4. lemma OAI.Coulomb.packetAnalysis_integral line 86
5. lemma OAI.Coulomb.packetAnalysis_measurable line 92
6. lemma OAI.Coulomb.packetAnalysis_momentum line 104
7. lemma OAI.Coulomb.packetAnalysis_momentum_integrable line 110
8. lemma OAI.Coulomb.packetWindowed_joint_integrable line 113
9. lemma OAI.Coulomb.packetWindowed_joint_integral line 130
10. lemma OAI.Coulomb.packetAnalysis_integrable line 137
11. lemma OAI.Coulomb.packetAnalysis_resolution line 145
12. def OAI.Coulomb.packetState line 157
13. lemma OAI.Coulomb.packetState_apply line 159
14. lemma OAI.Coulomb.packetState_norm line 178
15. lemma OAI.Coulomb.packetState_integral_norm_sq line 182
16. lemma OAI.Coulomb.packetState_inner line 186
17. lemma OAI.Coulomb.packetAnalysis_continuous line 200