OAI/Probability/SKRatio/Matrices/StandardGaussianProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKRatioGaussian.hasDerivAt_gaussianPDFReal line 12
2. theorem OAI.SKRatioGaussian.integrable_gaussian_iff line 25
3. theorem OAI.SKRatioGaussian.gaussian_integration_by_parts line 32
4. def OAI.SKRatioGaussian.standardGaussianProduct line 60
5. instance OAI.SKRatioGaussian.(instance at line 63) line 63
6. theorem OAI.SKRatioGaussian.continuous_insertNth line 67
7. theorem OAI.SKRatioGaussian.gaussianProduct_coordinate_IBP line 77