proposition: Lemma DMC_BSC_prop m y : let d := dH y (f m) in W ``(y | f m) = ((1 - Prob.p p) ^ (n - d) * Prob.p p ^ d)%R.
proof: Proof. move=> d; rewrite DMCE. transitivity ((\prod_(i < n | (f m) ``_ i == y ``_ i) (1 - Prob.p p)) * (\prod_(i < n | (f m) ``_ i != y ``_ i) Prob.p p))%R. rewrite (bigID [pred i | (f m) ``_ i == y ``_ i]) /=; congr (_ * _). by apply eq_bigr => // i /eqP ->; rewrite /BSC.c fdist_binaryxx. apply eq_bigr => //= i /negbTE Hyi; by rewrite /BSC.c fdist_binaryE eq_sym Hyi. congr (_ * _). by rewrite big_const /= iter_mulR /= card_dHC. by rewrite big_const /= iter_mulR /= card_dH_vec. 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