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

[RemyDegenne]

Define sub-Gaussian random variables and prove Hoeffding's inequality.

---

• [x] depends on: #15140

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15140~~ By Dependent Issues (🤖). Happy coding!

[RemyDegenne]

I was definitely planning to add Azuma-Hoeffding at some point. But I can change this PR to do it now, no problem.

About bounded vs sub-Gaussian random variables: the proof of the bounded version I know has two steps, first prove that bounded in [a,b] implies sub-Gaussian with constant (b - a)^2/4 (that's Hoeffding's lemma), then use the sub-Gaussian version. I started proving Hoeffding's lemma on another branch.

[RemyDegenne]

Update on this: I will introduce a more general property stating that a random variable has its cgf bounded from above by some function (or the same on the mgf, I am not sure yet), as well as a conditional version of that property (conditional sub-gaussian is what it needed for the sub-gaussian Azuma-Hoeffding). Then I can state that any bounded random variable has cgf bounded by the one of a Bernoulli and define subgaussian as a particular case of the dominated cgf property.

I mark this PR as WIP for now and will do that work in several of other PRs.