proposition: Theorem BSC_capacity : capacity (BSC.c card_A p_01) = 1 - H2 p.
proof: Proof. rewrite /capacity /image. set E := (fun y : R => _). set p' := Prob.mk_ p_01'_. have has_sup_E : has_sup E. split. set d := fdist_binary card_A p' (Set2.a card_A). by exists (`I(d, BSC.c card_A p')), d. exists 1 => y [P _ <-{y}]. have := IPW card_A P p_01'. set tmp := (X in `I(_, BSC.c _ X)). rewrite (_ : tmp = p_01)//; last first. by apply/val_inj => //. move=> ->. apply/RleP/leR_subl_addr/(leR_trans (H_out_max card_A P p_01')). rewrite addRC -leR_subl_addr subRR. by rewrite (entropy_H2 card_A (Prob.mk_ (p_01'_))); exact/entropy_ge0. apply eqR_le; split. apply/RleP. have [_ /(_ (1 - H2 p))] := Rsup_isLub (0 : R) has_sup_E. apply => x [d _ dx]; apply/RleP. suff : `H(d `o BSC.c card_A p_01) <= 1. have := IPW card_A d p_01'. set tmp := (X in `I(_, BSC.c _ X)). rewrite (_ : tmp = p_01)//; last first. by apply/val_inj => //. set tmp' := (X in _ = `H(d `o (BSC.c card_A X)) - _ -> _). rewrite (_ : tmp' = p_01)//; last first. by apply/val_inj => //. rewrite dx => -> ?. by rewrite leR_subl_addr subRK. have := H_out_max card_A d p_01'. set tmp' := (X in `H(d `o (BSC.c card_A X)) <= _ -> _). rewrite (_ : tmp' = p_01)//. by apply/val_inj. move: (@IPW _ card_A (fdist_uniform card_A) _ p_01'). rewrite H_out_binary_uniform => <-. apply/RleP/Rsup_ub => //=. exists (fdist_uniform card_A) => //. do 2 f_equal. exact: val_inj. 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