OAI/Analysis/CoulombIonization/Localization/PacketFourier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombPackets.packet_fourier line 28
2. lemma OAI.CoulombPackets.packet_kinetic line 38
3. lemma OAI.CoulombPackets.tensorRight_hasSum line 55
4. lemma OAI.CoulombPackets.partialOccupation_kinetic_lintegral line 68
5. lemma OAI.CoulombPackets.partialOccupation_kinetic line 133
6. lemma OAI.CoulombPauli.tensorRight_hasSum_general line 167
7. def OAI.CoulombPackets.spinMarginal line 186
8. def OAI.CoulombPackets.HasWeakSpinPartialDerivative line 190
9. lemma OAI.CoulombPackets.spinMarginal_weak_derivative line 196
10. lemma OAI.CoulombPackets.spinMarginal_sum_norm line 217