Commit 2022-07-12 07:50 0039a198

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.