proposition: Lemma mutual_info_chanE : `I(P, W) = mutual_info (fdistX (P `X W)).
proof: Proof. rewrite /mutual_info_chan mutual_infoE -cond_entropy_chanE. by rewrite -[in RHS]addR_opp oppRB addRCA addRA fdistX_prod_out. Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy jfdist_cond