mathlib

b33d6d6e - feat(probability/strong_law): Lp version of the strong law of large numbers (#15392)

feat(probability/strong_law): Lp version of the strong law of large numbers (#15392) This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.