mathlib3

0973ad45 - feat(probability/strong_law): the strong law of large numbers (#13690)

feat(probability/strong_law): the strong law of large numbers (#13690) We prove the almost sure version of the strong law of large numbers: given an iid sequence of integrable random variables `X_i`, then `(\sum_{i < n} X_i)/n` converges almost surely to `E(X)`. We follow Etemadi's proof, which only requires pairwise independence instead of full independence.