Integration results for finite independent random variables

Stream: Is there code for X?

[Kei TSUKAMOTO]

In mathlib, the equation E[X * Y] = E[X] * E[Y]has already formalized for two independent random variables X and Y, but is there any general formalization that states the finite case Π (i : Finset ℕ) , E [X i] = E [Π i, X (i : Finset ℕ)] where X i is independent?