OAI/Probability/SKGap/Gaussian/GaussianCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.gaussianCoordinates line 52
2. instance OAI.SKGap.(instance at line 55) line 55
3. def OAI.SKGap.gaussianAffine line 59
4. def OAI.SKGap.gaussianSup line 62
5. theorem OAI.SKGap.continuous_gaussianAffine line 66
6. theorem OAI.SKGap.gaussianSup_attained line 72
7. theorem OAI.SKGap.gaussianSup_le line 80
8. theorem OAI.SKGap.continuous_gaussianSup line 88
9. theorem OAI.SKGap.integrable_gaussianSup line 97
10. theorem OAI.SKGap.gaussianSup_comparison line 127