proposition: Lemma fdist_outE b : fdist_out b = \sum_(a in A) W a b * P a.
proof: Proof. by rewrite /fdist_out; unlock; rewrite ffunE. 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