Commit 2021-02-23 17:14 e3d6cf82

feat(measure_theory/integration): add theorems about the product of independent random variables (#6106) Consider the integral of the product of two random variables. Two random variables are independent if the preimage of all measurable sets are independent variables. Alternatively, if there is a pair of independent measurable spaces (as sigma algebras are independent), then two random variables are independent if they are measurable with respect to them.