proposition: Lemma Ex_comp_RV : `E (phi `o X) = \sum_(r <- fin_img X) phi r * `Pr[ X = r ].
proof: Proof. rewrite /Ex. rewrite (partition_big_fin_img _ X (fun u => (phi `o X) u * P u)) /=. apply: eq_bigr => a _. rewrite pr_eqE /Pr big_distrr /=; apply eq_big. by move=> u; rewrite inE. by move=> u /eqP Xua; rewrite /comp_RV -Xua. 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