mathlib3

4e1102a0 - feat(probability/integration): characterize indep_fun by expected product of comp (#13270)

feat(probability/integration): characterize indep_fun by expected product of comp (#13270) This is the third PR into probability/integration, to characterize independence by the expected product of compositions.