OAI/Probability/SKGap/Gaussian/GaussianSquareTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.gaussian_square_exp_integral line 12
2. lemma OAI.SKGap.gaussian_square_exp_integrable line 34
3. lemma OAI.SKGap.product_gaussian_square_exp_integral line 49
4. lemma OAI.SKGap.product_gaussian_square_exp_integrable line 62
5. lemma OAI.SKGap.product_gaussian_square_tail line 70
6. lemma OAI.SKGap.gaussian_scaled_coordinates_hasLaw line 95
7. lemma OAI.SKGap.scaled_gaussian_square_tail line 111
8. lemma OAI.SKGap.gaussian_real_square_tail line 133
9. lemma OAI.SKGap.gaussian_real_abs_tail line 141