OAI/Analysis/CoulombIonization/RadialBounds/WeakWindowMoment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.weak_window_moment line 21
2. lemma OAI.CoulombAtom.norm_complex_real_combination line 40
3. lemma OAI.CoulombAtom.integrable_shift_mul line 48
4. lemma OAI.CoulombAtom.integral_shift_mul line 58
5. lemma OAI.CoulombAtom.schwartz_integrable_sq line 64
6. lemma OAI.CoulombAtom.integral_schwartz_self_derivative line 68
7. lemma OAI.CoulombAtom.weak_window_derivative_integrable line 75
8. lemma OAI.CoulombAtom.integrated_weak_window_derivative line 91
9. lemma OAI.CoulombAtom.integrated_weak_window_moment line 118
10. lemma OAI.CoulombAtom.weak_window_fourier_measurable line 127
11. lemma OAI.CoulombAtom.weak_window_moment_integrable line 146
12. lemma OAI.CoulombAtom.weak_window_mass line 167
13. lemma OAI.CoulombAtom.weak_window_kinetic line 186