proposition: Lemma H_out_binary_uniform : `H(fdist_uniform card_A `o BSC.c card_A p_01) = 1.
proof: Proof. rewrite {1}/entropy !Set2sumE /= !fdist_outE !Set2sumE /=. rewrite /BSC.c !fdist_binaryxx !fdist_binaryE (eq_sym _ (Set2.a _)) !fdist_uniformE. rewrite (negbTE (Set2.a_neq_b card_A)). rewrite -!mulrDl. rewrite /onem subrK. rewrite !mul1r. rewrite addrC subrK. have ? : 2%mcR != 0%mcR :> R. rewrite (_ : 2%mcR = 2)//. rewrite (_ : 0%mcR = 0)//. by apply/eqP. rewrite -RdivE// ?card_A//. rewrite div1R -RinvE//. rewrite -!mulRDl /log LogV//. rewrite Log_n //=. rewrite (_ : 2%mcR = 2)//. field. 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