proposition: Lemma Pr_fdist_prod (A B : finType) (P1 : {fdist A}) (P2 : {fdist B}) (E1 : {set A}) (E2 : {set B}) : Pr (P1 `x P2) ((E1 `*T) :&: (T`* E2)) = Pr (P1 `x P2) (E1 `*T) * Pr (P1 `x P2) (T`* E2).
proof: Proof. rewrite {1}/Pr /=. set P := P1 `x P2. rewrite (eq_bigr (fun x => P (x.1, x.2))); last by case. rewrite [in LHS](eq_bigl (fun x => (x.1 \in E1) && (x.2 \in E2))); last first. by case=> a b; rewrite !inE. rewrite -[in LHS](pair_big _ _ (fun x1 x2 => P (x1, x2))) /=. rewrite {1}/Pr /=. rewrite (eq_bigr (fun x => P (x.1, x.2))); last by case. rewrite [in X in _ = X * _](eq_bigl (fun a => a.1 \in E1)); last first. by case=> a b; rewrite !inE. rewrite [in RHS](eq_bigl (fun x => (x.1 \in E1) && true)); last first. by case=> a b; rewrite !andbT. rewrite -[in RHS](pair_big (fun x => x \in E1) xpredT (fun x1 x2 => P (x1, x2))) /=. rewrite big_distrl /=; apply eq_big => // a /eqP E1a /=. rewrite {1}/Pr /=. rewrite (eq_bigr (fun x => P (x.1, x.2))); last by case. rewrite [in X in _ = _ * X](eq_bigl (fun a => a.2 \in E2)); last first. by move=> b; rewrite !inE. rewrite [in RHS](eq_bigl (fun x => true && (x.2 \in E2))) //. rewrite -[in RHS](pair_big xpredT (fun x => x \in E2) (fun x1 x2 => P (x1, x2))) /=. rewrite exchange_big /= big_distrr /=; apply eq_big => // b E2b. rewrite fdist_prodE /=; congr (_ * _); under eq_bigr do rewrite fdist_prodE /=. by rewrite -big_distrr /= FDist.f1 mulR1. by rewrite -big_distrl /= FDist.f1 mul1R. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist