proposition: Lemma DMC_sub_vecE (V : {set 'I_n}) (t : 'rV_n) : W ``(tb \# V | t \# V) = \prod_(i in V) W (t ``_ i) (tb ``_ i).
proof: Proof. by rewrite DMCE -rprod_sub_vec. 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