proposition: Lemma ML_smallest_err_rate phi : echa(W, mkCode enc dec) <= echa(W, mkCode enc phi).
proof: Proof. apply/RleP/leR_wpmul2l; first by apply/mulR_ge0 => //; exact/invR_ge0/ltR0n. rewrite /ErrRateCond /=; apply/RleP. rewrite [leRHS](eq_bigr (fun m => 1 - Pr (W ``(|enc m)) [set tb | phi tb == Some m])); last first. move=> m _; rewrite Pr_to_cplt; congr (_ - Pr _ _). apply/setP => t; by rewrite !inE negbK. rewrite [leLHS](eq_bigr (fun m => 1 - Pr (W ``(|enc m)) [set tb | dec tb == Some m])); last first. move => m _. rewrite [in LHS]Pr_to_cplt; congr (_ - Pr _ _). apply/setP => t; by rewrite !inE negbK. rewrite 2!big_split /=; apply: lerD => //. rewrite -2!big_morph_oppR lerNr opprK /Pr (exchange_big_dep xpredT) //=. rewrite [leRHS](exchange_big_dep xpredT) //=. apply ler_sum => /= tb _. rewrite (eq_bigl (fun m => phi tb == Some m)); last by move=> m; rewrite inE. rewrite [leRHS](eq_bigl (fun m => dec tb == Some m)); last by move=> m; rewrite inE. have [dectb_None|dectb_Some] := boolP (dec tb == None). case/boolP : (receivable_prop P W tb) => [Hy|Htb]. case: (ML_dec (mkReceivable Hy)) => [m' [tb_m']]. by move: dectb_None; rewrite {1}/dec {1}ffunE tb_m'. have W_tb m : W ``(tb | enc m) = 0%R. apply/eqP; apply/contraR : Htb => Htb. apply/existsP; exists (enc m). rewrite Htb andbT fdist_uniform_supp_neq0 inE. move/subsetP : enc_img; apply; apply/imsetP; by exists m. rewrite (eq_bigr (fun=> 0)); last by move=> m _; rewrite W_tb. by rewrite big1 //; apply sumr_ge0. case/boolP : (phi tb == None) => [/eqP ->|phi_tb]. by rewrite big_pred0 //; apply sumr_ge0. have [m1 Hm1] : exists m', dec tb = Some m' by destruct (dec tb) => //; exists s. have [m2 Hm2] : exists m', phi tb = Some m' by destruct (phi tb) => //; exists s. rewrite Hm1 {}Hm2. rewrite (eq_bigl [pred m | m == m2]); last by move=> ?; rewrite eq_sym. rewrite [leRHS](eq_bigl [pred m | m == m1]); last by move=> ?; rewrite eq_sym. rewrite 2!big_pred1_eq; apply ML_err_rate. move: Hm1; rewrite /dec ffunE /omap /obind /oapp. move H : (repair tb) => h. case: h H => // a tb_a [<-]; congr Some. by rewrite (discard_cancel tb_a). by move/subsetP : enc_img; apply; apply/imsetP; exists m2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg perm) mathcomp(zmodp matrix vector order) mathcomp(lra mathcomp_extra Rstruct reals) Reals ssrR realType_ext Reals_ext ssr_ext ssralg_ext f2 fdist proba channel_code channel binary_symmetric_channel hamming pproba