proposition: Lemma channel_jcPr (A B : finType) (W : `Ch(A, B)) (P : {fdist A}) a b : P a != 0 -> W a b = \Pr_(fdistX (P `X W))[ [set b] | [set a] ].
proof: Proof. by move=> Pa0; rewrite jcPr_fdistX_prod//; exact/eqP. 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