proposition: Lemma bsc_post (a : A) : (P `^ 1) `^^ (BSC.c card_A p_01) (\row_(i < 1) a | mkReceivable Ha') = (if a == a' then 1 - p else p)%R.
proof: Proof. rewrite fdist_post_probE /= !fdist_rVE DMCE big_ord_recl big_ord0. rewrite (eq_bigr (fun x : 'M_1 => P a * (BSC.c card_A p_01) ``( (\row__ a') | x))%R); last first. by move=> i _; rewrite /P !fdist_rVE big_ord_recl big_ord0 !fdist_uniformE mulr1. rewrite -big_distrr /= (_ : \sum_(_ | _) _ = 1)%R; last first. transitivity (\sum_(i in 'M_1) fdist_binary card_A p_01 (i ``_ ord0) a')%R. apply eq_bigr => i _. by rewrite DMCE big_ord_recl big_ord0 mulR1 /BSC.c mxE. apply/(@big_rV1_ord0 _ _ _ _ (fdist_binary card_A p_01 ^~ a')). by rewrite -sum_fdist_binary_swap // FDist.f1. rewrite mxE mulr1 big_ord_recl big_ord0 /BSC.c fdist_binaryE /= eq_sym !mxE. rewrite !coqRE mulr1 onemE. rewrite mulrAC mulfV ?mul1r // fdist_uniformE card_A invr_neq0 //. by apply: lt0r_neq0; lra. 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