OAI/Probability/StrongRayleigh/GaussianMomentBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336AdditiveD139.GaussianMomentBounds.standardThirdAbsMoment line 14
2. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.standardThirdAbsMoment_nonneg line 16
3. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_sq_gaussianReal line 19
4. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_abs_gaussianReal_le line 25
5. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.gaussianReal_map_sqrt line 39
6. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_abs_pow_gaussianReal line 47
7. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_abs_cube_gaussianReal line 54
8. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integrable_abs_pow_gaussianReal line 62
9. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_eq_zero_of_hasLaw line 72
10. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_sq_of_hasLaw line 76
11. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_abs_le_of_hasLaw line 83
12. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integral_abs_cube_of_hasLaw line 90
13. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integrable_abs_pow_of_hasLaw line 97
14. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integrable_of_hasLaw line 103
15. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.integrable_sq_of_hasLaw line 108
16. lemma OAI.Problem336AdditiveD139.GaussianMomentBounds.conditional_gaussian_moments line 119