mathlib3

56065f7e - feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. (#6353)

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 Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>