OAI/Analysis/CoulombIonization/Variational/SmoothCompactIntegral.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.firstPartial line 24
2. lemma OAI.CoulombAtom.firstPartial_hasFDerivAt line 29
3. lemma OAI.CoulombAtom.firstPartial_contDiff line 36
4. lemma OAI.CoulombAtom.weightedSetIntegral_hasFDerivAt line 40
5. lemma OAI.CoulombAtom.weightedSetIntegral_contDiff_nat line 64
6. lemma OAI.CoulombAtom.weightedSetIntegral_contDiff line 86
7. def OAI.CoulombAtom.coherentSpatialSupport line 99
8. lemma OAI.CoulombAtom.coherentSpatialSupport_compact line 102
9. lemma OAI.CoulombAtom.coherentPacket_zero_outside line 106
10. lemma OAI.CoulombAtom.coherentPacket_joint_smooth line 115
11. def OAI.CoulombAtom.packetSynthesis line 122
12. lemma OAI.CoulombAtom.packetSynthesis_smooth line 126
13. lemma OAI.CoulombAtom.packetSynthesis_zero_outside line 135
14. lemma OAI.CoulombAtom.packetSynthesis_compact line 143
15. lemma OAI.CoulombAtom.coherent_test_integrable line 152
16. lemma OAI.CoulombAtom.coherentVector_inner_schwartz_left line 170
17. lemma OAI.CoulombAtom.packetSynthesis_test line 180
18. lemma OAI.CoulombAtom.packetSynthesis_memLp line 199
19. lemma OAI.CoulombAtom.coherentVector_weight_integrable line 206
20. lemma OAI.CoulombAtom.packetSynthesis_toLp line 214