Commit 2023-09-26 13:13 c8812942

feat: strong law of large numbers for vector-valued random variables (#7218) We already have the strong law of large numbers for real-valued integrable random variables. We generalize it to general vector-valued integrable random variables. This does not require any second-countability assumptions as integrable functions can by definition be approximated by simple functions, for which the result is deduced from the one-dimensional one. Along the way, we extend a few lemmas in the library from the real case to the vector case, and remove unneeded second-countability assumptions.