OAI/Probability/GaussianPropeller/PairIntegral.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.PairIntegral.integrableOn_pos_sub_pow line 35
2. lemma OAI.GaussianPropeller.PairIntegral.integral_pos_sub_pow line 51
3. lemma OAI.GaussianPropeller.PairIntegral.lintegral_pos_sub_pow line 71
4. lemma OAI.GaussianPropeller.PairIntegral.lintegral_triangle_shifted line 77
5. lemma OAI.GaussianPropeller.PairIntegral.gaussianPDF_std_le line 92
6. lemma OAI.GaussianPropeller.PairIntegral.lintegral_gaussian_std_le line 99
7. lemma OAI.GaussianPropeller.PairIntegral.lintegral_affine_volume line 111
8. lemma OAI.GaussianPropeller.PairIntegral.lintegral_affine_gaussian_le line 121
9. def OAI.GaussianPropeller.PairIntegral.triangle line 133
10. lemma OAI.GaussianPropeller.PairIntegral.measurable_triangle line 136
11. lemma OAI.GaussianPropeller.PairIntegral.lintegral_triangle line 142
12. lemma OAI.GaussianPropeller.PairIntegral.lintegral_gaussian_pair_le line 172
13. lemma OAI.GaussianPropeller.PairIntegral.integral_pos_cube_gaussian line 199
14. lemma OAI.GaussianPropeller.PairIntegral.integrable_pos_cube_gaussian line 232
15. lemma OAI.GaussianPropeller.PairIntegral.lintegral_pos_cube_gaussian line 242
16. lemma OAI.GaussianPropeller.PairIntegral.lintegral_triangle_gaussian line 248
17. lemma OAI.GaussianPropeller.PairIntegral.integral_le_of_lintegral_ofReal_le line 280