mathlib3

feat(probability/subgaussian): define sub-Gaussian random variables

#15141

Open