proposition: Lemma HP_HPW : `H P - `H(P, BSC.c card_A p_01) = - H2 p.
proof: Proof. rewrite {2}/entropy /=. rewrite (eq_bigr (fun a => ((P `X (BSC.c card_A p_01))) (a.1, a.2) * log (((P `X (BSC.c card_A p_01))) (a.1, a.2)))); last by case. rewrite -(pair_big xpredT xpredT (fun a b => (P `X (BSC.c card_A p_01)) (a, b) * log ((P `X (BSC.c card_A p_01)) (a, b)))) /=. rewrite {1}/entropy . set a := \sum_(_ in _) _. set b := \sum_(_ <- _) _. apply trans_eq with (- (a + (-1) * b)); first by field. rewrite /b {b} big_distrr /= /a {a} -big_split /=. rewrite !Set2sumE /= !fdist_prodE /BSC.c !fdist_binaryxx !fdist_binaryE/=. rewrite eq_sym !(negbTE (Set2.a_neq_b card_A)) /H2 . set a := Set2.a _. set b := Set2.b _. case: (Req_EM_T (P a) 0) => H1. rewrite H1 !(mul0R, mulR0, addR0, add0R). move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b. rewrite H1 add0r => ->. rewrite /log Log_1 -!RmultE !(mul0R, mulR0, addR0, add0R, mul1R, mulR1). rewrite /onem -RminusE (_ : 1%mcR = 1)//. field. rewrite /log LogM; last 2 first. move/eqP in H1. have [+ _] := fdist_gt0 P a. by move/(_ H1) => /RltP. by case/andP: p_01' => ? ?; exact/RltP/onem_gt0. rewrite /log LogM; last 2 first. move/eqP in H1. have [+ _] := fdist_gt0 P a. by move/(_ H1) => /RltP. by case/andP: p_01' => ? ?; exact/RltP. case: (Req_EM_T (P b) 0) => H2. rewrite H2 !(mul0R, mulR0, addR0, add0R). move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b. rewrite H2 addr0 => ->. rewrite /log Log_1 -!RmultE !(mul0R, mulR0, addR0, add0R, mul1R, mulR1). rewrite /onem -RminusE (_ : 1%mcR = 1)//. field. rewrite /log LogM; last 2 first. move/eqP in H2. have [+ _] := fdist_gt0 P b. by move/(_ H2) => /RltP. by case/andP: p_01' => ? ?; exact/RltP. rewrite /log LogM; last 2 first. move/eqP in H2. have [+ _] := fdist_gt0 P b. by move/(_ H2) => /RltP. by case/andP: p_01' => ? ?; exact/RltP/onem_gt0. rewrite /log. rewrite -!RmultE. rewrite /onem -RminusE (_ : 1%mcR = 1)//. transitivity (p * (P a + P b) * log p + (1 - p) * (P a + P b) * log (1 - p) ). rewrite /log. set l2Pa := Log 2 (P a). set l2Pb := Log 2 (P b). set l21p := Log 2 (1 - p). set l2p := Log 2 p. ring_simplify. congr (_ + _). rewrite [RHS]addRC !addRA; congr (_ + _). rewrite [RHS]addRC !addRA; congr (_ + _). rewrite [RHS]addRC !addRA; congr (_ + _ + _). rewrite !mulNR; congr (- _). by rewrite [RHS]mulRC mulRA. by rewrite [RHS]mulRC mulRA. by rewrite mulRC. move: (FDist.f1 P). rewrite Set2sumE /= -/a -/b. rewrite -RplusE => ->. rewrite !mulR1. rewrite /log; 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