proposition: Lemma IPW : `I(P, BSC.c card_A p_01) = `H(P `o BSC.c card_A p_01) - H2 p.
proof: Proof. rewrite /mutual_info_chan addRC. set a := `H(_ `o _). transitivity (a + (`H P - `H(P , BSC.c card_A p_01))); first by field. by rewrite HP_HPW. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum zmodp matrix lra) mathcomp(mathcomp_extra classical_sets Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist entropy binary_entropy_function channel hamming channel_code pproba