proposition: Lemma cond_entropy_chanE2 : `H(W | P) = \sum_(a in A) P a * `H (W a).
proof: Proof. rewrite cond_entropy_chanE cond_entropyE big_morph_oppR; apply: eq_bigr => a _. rewrite big_morph_oppR /entropy mulRN -mulNR big_distrr/=; apply: eq_bigr => b _. rewrite fdistXI fdist_prodE /= mulNR mulRA; congr (- _). have [->|Pa0] := eqVneq (P a) 0; first by rewrite -RmultE !(mulR0,mul0R). by rewrite -channel_jcPr. 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