OAI/Probability/SKRatio/Matrices/GaussianCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.gaussianCoordinates line 53
2. instance OAI.SKRatioGaussian.(instance at line 56) line 56
3. def OAI.SKRatioGaussian.gaussianAffine line 60
4. def OAI.SKRatioGaussian.gaussianSup line 63
5. theorem OAI.SKRatioGaussian.continuous_gaussianAffine line 67
6. theorem OAI.SKRatioGaussian.gaussianSup_attained line 73
7. theorem OAI.SKRatioGaussian.gaussianSup_le line 81
8. theorem OAI.SKRatioGaussian.continuous_gaussianSup line 89
9. theorem OAI.SKRatioGaussian.integrable_gaussianSup line 98
10. theorem OAI.SKRatioGaussian.gaussianSup_comparison line 128