mathlib3

0039a198 - feat(probability/independence): two tuples indexed by disjoint subsets of an independent family of r.v. are independent (#15131)

feat(probability/independence): two tuples indexed by disjoint subsets of an independent family of r.v. are independent (#15131) If `f` is a family of independent random variables and `S,T` are two disjoint finsets, then we have `indep_fun (λ a (i : S), f i a) (λ a (i : T), f i a) μ`. Also golf `indep_fun_iff_measure_inter_preimage_eq_mul` and add its `Indep` version: `Indep_fun_iff_measure_inter_preimage_eq_mul`.