OAI/Analysis/CoulombIonization/Localization/SubGaussianMoments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombObservation.even_pow_le_factorial_exp line 16
2. lemma OAI.CoulombObservation.subGaussian_even_moment_integrable line 28
3. theorem OAI.CoulombObservation.subGaussian_even_moment_le line 37
4. def OAI.CoulombObservation.observationSign line 106
5. def OAI.CoulombObservation.signLaw line 108
6. instance OAI.CoulombObservation.signLaw_probability line 110
7. lemma OAI.CoulombObservation.observationSign_subGaussian line 114
8. def OAI.CoulombObservation.signProduct line 126
9. instance OAI.CoulombObservation.signProduct_probability line 129
10. lemma OAI.CoulombObservation.observationSign_eval_subGaussian line 134
11. lemma OAI.CoulombObservation.sign_sum_subGaussian line 144
12. theorem OAI.CoulombObservation.sign_sum_even_moment_le line 158