proposition: Lemma H_out_max : `H(P `o BSC.c card_A p_01) <= 1.
proof: Proof. rewrite {1}/entropy /= Set2sumE /= !fdist_outE 2!Set2sumE /=. set a := Set2.a _. set b := Set2.b _. rewrite /BSC.c !fdist_binaryxx !fdist_binaryE /= !(eq_sym _ a). rewrite (negbTE (Set2.a_neq_b card_A)). move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b => P1. rewrite -!(RmultE,RplusE). have -> : p * P a + (1 - p) * P b = 1 - ((1 - p) * P a + p * P b). rewrite -RplusE (_ : 1%mcR = 1)// in P1. rewrite -{2}P1. ring_simplify. congr (_ + _). by rewrite subRK. case/andP: p_01' => /RltP Hp1 /RltP Hp2. rewrite (_ : 0%mcR = 0%coqR)// in Hp1. rewrite (_ : 1%mcR = 1%coqR)// in Hp2, P1. have H01 : 0 < ((1 - p) * P a + p * P b) < 1. move: (FDist.ge0 P a) => /RleP H1. move: (FDist.le1 P b) => H4. move: (FDist.le1 P a) => H3. split. case/Rle_lt_or_eq_dec : H1 => H1; rewrite (_ : 0%mcR = 0)// in H1. - apply addR_gt0wl. apply: mulR_gt0 => //. by rewrite subR_gt0. apply: mulR_ge0 => //. exact: ltRW. - by rewrite -H1 mulR0 add0R (_ : P b = 1) ?mulR1 // -P1 -H1 add0r. rewrite -{2}P1. case: (Req_EM_T (P a) 0) => Hi. rewrite Hi mulR0 !add0R. rewrite Hi add0r in P1. by rewrite P1 mulR1 add0r. case: (Req_EM_T (P b) 0) => Hj. rewrite Hj addr0 in P1. rewrite Hj mulR0 !addR0 P1 mulR1. rewrite addr0. by rewrite ltR_subl_addr ltR_addl. case/Rle_lt_or_eq_dec : H1 => H1. - apply leR_lt_add. + rewrite -{2}(mul1R (P a)); apply leR_wpmul2r => //. by rewrite leR_subl_addr leR_addl; exact: ltRW. + rewrite -{2}(mul1R (P b)); apply ltR_pmul2r => //. by apply/RltP; rewrite lt0r; apply/andP; split; [exact/eqP|by []]. - rewrite -H1 mulR0 add0R add0r. have -> : P b = 1 by rewrite -P1 -H1 add0r. by rewrite mulR1. rewrite (_ : forall a b, - (a + b) = - a - b); last by move=> *; field. rewrite -mulNR. set q := (1 - p) * P a + p * P b. apply: (@leR_trans (H2 q)); last exact: H2_max. by rewrite /H2 !mulNR; apply Req_le; 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