Commit 2021-03-11 11:19 56065f7e

feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. (#6353) The goal here is to prove that the expectation of a product of an finite number of independent random variables equals the production of the expectations. See https://github.com/leanprover-community/mathlib/tree/mzinkevi_independent_finite_alt