OAI/Probability/SKGap/Gaussian/StandardGaussianProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGap.hasDerivAt_gaussianPDFReal line 11
2. theorem OAI.SKGap.integrable_gaussian_iff line 24
3. theorem OAI.SKGap.gaussian_integration_by_parts line 31
4. def OAI.SKGap.standardGaussianProduct line 59
5. instance OAI.SKGap.(instance at line 62) line 62
6. theorem OAI.SKGap.continuous_insertNth line 66
7. theorem OAI.SKGap.gaussianProduct_coordinate_IBP line 76
8. lemma OAI.SKGap.tendsto_gaussianPDFReal_atTop line 129
9. lemma OAI.SKGap.tendsto_gaussianPDFReal_neg_atTop line 143
10. theorem OAI.SKGap.gaussian_lipschitz_IBP line 153