proposition: Lemma E_prod_2 : inde_rv X' Y' -> `E XmY = `E X * `E Y.
proof: Proof. move=> Hinde. transitivity (\sum_(x <- fin_img X) \sum_(y <- fin_img Y) x * y * `Pr[ XY = (x, y) ]). rewrite /Ex /= (eq_bigr (fun u => X u.1 * Y u.2 * P (u.1, u.2))); last by case. rewrite -(pair_bigA _ (fun u1 u2 => X u1 * Y u2 * P (u1, u2))) /=. rewrite (partition_big_fin_img _ X) /=; apply eq_bigr => x _. rewrite exchange_big /= (partition_big_fin_img _ Y) /=; apply eq_bigr => y _. rewrite pr_eqE /Pr big_distrr /= exchange_big pair_big /=. apply eq_big. by move=> -[a b] /=; rewrite inE. by case=> a b /= /andP[/eqP -> /eqP ->]. transitivity (\sum_(x <- fin_img X) \sum_(y <- fin_img Y) x * y * `Pr[ X = x ] * `Pr[ Y = y ]). apply eq_bigr => x _; apply eq_bigr => y _. rewrite -!mulRA. have {}Hinde := Hinde x y. congr (_ * (_ * _)). transitivity (`Pr[ X' = x ] * `Pr[ Y' = y ]); last first. congr (_ * _). rewrite !pr_eqE Pr_fdist_fst; congr Pr. by apply/setP => -[a b]; rewrite !inE. rewrite !pr_eqE Pr_fdist_snd; congr Pr. by apply/setP => -[a b]; rewrite !inE. by rewrite -Hinde !pr_eqE. rewrite -!Ex_altE. rewrite /Ex_alt big_distrl; apply eq_bigr => x _ /=; rewrite big_distrr /=. apply eq_bigr=> y _. by rewrite -!mulRA; congr (_ * _); rewrite mulRCA. 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