Proposal: Norm of matrices with gaussian entries

[tukamilano]

I'd like to formalize The 4.4.3, 4.4.7, 4.6.1 in high dimensional probability. Some theorem around subgaussian's property are needed to formalize

[tukamilano]

I noticed that this overlaps with the existing code.
So the only change I'll actually make is to use Exercise 4.43 to relax independence in Thm 4.4.3.

[tukamilano]

merged #53